diff --git a/Mathlib.lean b/Mathlib.lean
index c66a3419a9aeb..e24762ba7699b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -544,6 +544,10 @@ import Mathlib.Algebra.MvPolynomial.Rename
 import Mathlib.Algebra.MvPolynomial.Supported
 import Mathlib.Algebra.MvPolynomial.Variables
 import Mathlib.Algebra.NeZero
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Pi
+import Mathlib.Algebra.NoZeroSMulDivisors.Prod
 import Mathlib.Algebra.Notation
 import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue
@@ -4443,7 +4447,6 @@ import Mathlib.Tactic.ReduceModChar
 import Mathlib.Tactic.ReduceModChar.Ext
 import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm
-import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
index 66932daf4008d..e9e129ad5c0fd 100644
--- a/Mathlib/Algebra/Algebra/Basic.lean
+++ b/Mathlib/Algebra/Algebra/Basic.lean
@@ -9,6 +9,7 @@ import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.Algebra.Module.Submodule.Ker
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.Module.ULift
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Ring.Subring.Basic
 import Mathlib.Data.Nat.Cast.Order.Basic
 import Mathlib.Data.Int.CharZero
diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
index fbfabaaebfca3..b6b2d96428073 100644
--- a/Mathlib/Algebra/BigOperators/Finprod.lean
+++ b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -5,7 +5,7 @@ Authors: Kexing Ying, Kevin Buzzard, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
 import Mathlib.Algebra.Group.FiniteSupport
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Set.Subsingleton
 
diff --git a/Mathlib/Algebra/Group/EvenFunction.lean b/Mathlib/Algebra/Group/EvenFunction.lean
index 4713a0549c61f..81ddf35dcd57c 100644
--- a/Mathlib/Algebra/Group/EvenFunction.lean
+++ b/Mathlib/Algebra/Group/EvenFunction.lean
@@ -3,9 +3,9 @@ Copyright (c) 2024 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
-import Mathlib.Algebra.Group.Action.Pi
-import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.BigOperators.Group.Finset
+import Mathlib.Algebra.Group.Action.Pi
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 
 /-!
 # Even and odd functions
diff --git a/Mathlib/Algebra/ModEq.lean b/Mathlib/Algebra/ModEq.lean
index a275aad2c7254..2744ba932b93f 100644
--- a/Mathlib/Algebra/ModEq.lean
+++ b/Mathlib/Algebra/ModEq.lean
@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Int.ModEq
 import Mathlib.Algebra.Field.Basic
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.GroupTheory.QuotientGroup.Basic
 
diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
index 8656e47667f24..18deb70317a22 100644
--- a/Mathlib/Algebra/Module/Basic.lean
+++ b/Mathlib/Algebra/Module/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.Group.Indicator
 import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
 # Further basic results about modules.
@@ -95,30 +96,6 @@ theorem inv_intCast_smul_comm {α E : Type*} (R : Type*) [AddCommGroup E] [Divis
 @[deprecated (since := "2024-04-17")]
 alias inv_int_cast_smul_comm := inv_intCast_smul_comm
 
-
-
-section NoZeroSMulDivisors
-
-section Module
-
-instance [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
-  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ c x, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩
-
-end Module
-
-section GroupWithZero
-
-variable [GroupWithZero R] [AddMonoid M] [DistribMulAction R M]
-
--- see note [lower instance priority]
-/-- This instance applies to `DivisionSemiring`s, in particular `NNReal` and `NNRat`. -/
-instance (priority := 100) GroupWithZero.toNoZeroSMulDivisors : NoZeroSMulDivisors R M :=
-  ⟨fun {a _} h ↦ or_iff_not_imp_left.2 fun ha ↦ (smul_eq_zero_iff_eq <| Units.mk0 a ha).1 h⟩
-
-end GroupWithZero
-
-end NoZeroSMulDivisors
-
 namespace Function
 
 lemma support_smul_subset_left [Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) :
diff --git a/Mathlib/Algebra/Module/Card.lean b/Mathlib/Algebra/Module/Card.lean
index e9c8b1d5446ec..3941ffd972d1d 100644
--- a/Mathlib/Algebra/Module/Card.lean
+++ b/Mathlib/Algebra/Module/Card.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.SetTheory.Cardinal.Basic
 
 /-!
diff --git a/Mathlib/Algebra/Module/Defs.lean b/Mathlib/Algebra/Module/Defs.lean
index a024554de986a..c51d03d323fe8 100644
--- a/Mathlib/Algebra/Module/Defs.lean
+++ b/Mathlib/Algebra/Module/Defs.lean
@@ -408,182 +408,6 @@ instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCo
     [Module R M] : IsScalarTower ℤ R M where
   smul_assoc n x y := ((smulAddHom R M).flip y).map_zsmul x n
 
-section NoZeroSMulDivisors
-
-/-! ### `NoZeroSMulDivisors`
-
-This section defines the `NoZeroSMulDivisors` class, and includes some tests
-for the vanishing of elements (especially in modules over division rings).
--/
-
-
-/-- `NoZeroSMulDivisors R M` states that a scalar multiple is `0` only if either argument is `0`.
-This is a version of saying that `M` is torsion free, without assuming `R` is zero-divisor free.
-
-The main application of `NoZeroSMulDivisors R M`, when `M` is a module,
-is the result `smul_eq_zero`: a scalar multiple is `0` iff either argument is `0`.
-
-It is a generalization of the `NoZeroDivisors` class to heterogeneous multiplication.
--/
-@[mk_iff]
-class NoZeroSMulDivisors (R M : Type*) [Zero R] [Zero M] [SMul R M] : Prop where
-  /-- If scalar multiplication yields zero, either the scalar or the vector was zero. -/
-  eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0
-
-export NoZeroSMulDivisors (eq_zero_or_eq_zero_of_smul_eq_zero)
-
-/-- Pullback a `NoZeroSMulDivisors` instance along an injective function. -/
-theorem Function.Injective.noZeroSMulDivisors {R M N : Type*} [Zero R] [Zero M] [Zero N]
-    [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.Injective f)
-    (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M :=
-  ⟨fun {_ _} h =>
-    Or.imp_right (@hf _ _) <| h0.symm ▸ eq_zero_or_eq_zero_of_smul_eq_zero (by rw [← hs, h, h0])⟩
-
--- See note [lower instance priority]
-instance (priority := 100) NoZeroDivisors.toNoZeroSMulDivisors [Zero R] [Mul R]
-    [NoZeroDivisors R] : NoZeroSMulDivisors R R :=
-  ⟨fun {_ _} => eq_zero_or_eq_zero_of_mul_eq_zero⟩
-
-theorem smul_ne_zero [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M}
-    (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0 := fun h =>
-  (eq_zero_or_eq_zero_of_smul_eq_zero h).elim hc hx
-
-section SMulWithZero
-
-variable [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M}
-
-@[simp]
-theorem smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=
-  ⟨eq_zero_or_eq_zero_of_smul_eq_zero, fun h =>
-    h.elim (fun h => h.symm ▸ zero_smul R x) fun h => h.symm ▸ smul_zero c⟩
-
-theorem smul_ne_zero_iff : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 := by rw [Ne, smul_eq_zero, not_or]
-
-lemma smul_eq_zero_iff_left (hx : x ≠ 0) : c • x = 0 ↔ c = 0 := by simp [hx]
-lemma smul_eq_zero_iff_right (hc : c ≠ 0) : c • x = 0 ↔ x = 0 := by simp [hc]
-lemma smul_ne_zero_iff_left (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0 := by simp [hx]
-lemma smul_ne_zero_iff_right (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0 := by simp [hc]
-
-end SMulWithZero
-
-section Module
-
-section Nat
-
-theorem Nat.noZeroSMulDivisors
-    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] :
-    NoZeroSMulDivisors ℕ M where
-  eq_zero_or_eq_zero_of_smul_eq_zero {c x} := by rw [← Nat.cast_smul_eq_nsmul R, smul_eq_zero]; simp
-
-theorem two_nsmul_eq_zero
-    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : 2 • v = 0 ↔ v = 0 := by
-  haveI := Nat.noZeroSMulDivisors R M
-  simp [smul_eq_zero]
-
-end Nat
-
-variable [Semiring R]
-variable (R M)
-
-/-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
-zero as well. Usually `M` is an `R`-algebra. -/
-theorem CharZero.of_module (M) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R := by
-  refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩
-  rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
-
-end Module
-
-section AddCommGroup
-
--- `R` can still be a semiring here
-variable [Semiring R] [AddCommGroup M] [Module R M]
-
-section SMulInjective
-
-variable (M)
-
-theorem smul_right_injective [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) :
-    Function.Injective (c • · : M → M) :=
-  (injective_iff_map_eq_zero (smulAddHom R M c)).2 fun _ ha => (smul_eq_zero.mp ha).resolve_left hc
-
-variable {M}
-
-theorem smul_right_inj [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M} :
-    c • x = c • y ↔ x = y :=
-  (smul_right_injective M hc).eq_iff
-
-end SMulInjective
-
-section Nat
-
-theorem self_eq_neg
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : v = -v ↔ v = 0 := by
-  rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]
-
-theorem neg_eq_self
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : -v = v ↔ v = 0 := by
-  rw [eq_comm, self_eq_neg R M]
-
-theorem self_ne_neg
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : v ≠ -v ↔ v ≠ 0 :=
-  (self_eq_neg R M).not
-
-theorem neg_ne_self
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : -v ≠ v ↔ v ≠ 0 :=
-  (neg_eq_self R M).not
-
-end Nat
-
-end AddCommGroup
-
-section Module
-
-variable [Ring R] [AddCommGroup M] [Module R M]
-
-section SMulInjective
-
-variable (R)
-variable [NoZeroSMulDivisors R M]
-
-theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x :=
-  fun c d h =>
-  sub_eq_zero.mp
-    ((smul_eq_zero.mp
-          (calc
-            (c - d) • x = c • x - d • x := sub_smul c d x
-            _ = 0 := sub_eq_zero.mpr h
-            )).resolve_right
-      hx)
-
-end SMulInjective
-
-instance [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
-  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩
-
-variable (R M)
-
-theorem NoZeroSMulDivisors.int_of_charZero
-    (R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] :
-    NoZeroSMulDivisors ℤ M :=
-  ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩
-
-/-- Only a ring of characteristic zero can have a non-trivial module without additive or
-scalar torsion. -/
-theorem CharZero.of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R := by
-  refine ⟨fun {n m h} ↦ ?_⟩
-  obtain ⟨x, hx⟩ := exists_ne (0 : M)
-  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
-  simpa using smul_left_injective ℤ hx h
-
-end Module
-
-end NoZeroSMulDivisors
-
 -- Porting note (#10618): simp can prove this
 --@[simp]
 theorem Nat.smul_one_eq_cast {R : Type*} [NonAssocSemiring R] (m : ℕ) : m • (1 : R) = ↑m := by
diff --git a/Mathlib/Algebra/Module/LinearMap/Basic.lean b/Mathlib/Algebra/Module/LinearMap/Basic.lean
index 1a68ecbd89506..baff9dbf891d4 100644
--- a/Mathlib/Algebra/Module/LinearMap/Basic.lean
+++ b/Mathlib/Algebra/Module/LinearMap/Basic.lean
@@ -5,7 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
   Frédéric Dupuis, Heather Macbeth
 -/
 import Mathlib.Algebra.Module.LinearMap.Defs
-import Mathlib.Algebra.Module.Pi
+import Mathlib.Algebra.NoZeroSMulDivisors.Pi
 import Mathlib.GroupTheory.GroupAction.DomAct.Basic
 
 /-!
diff --git a/Mathlib/Algebra/Module/LinearMap/End.lean b/Mathlib/Algebra/Module/LinearMap/End.lean
index f75595188a8c1..a861127390ad8 100644
--- a/Mathlib/Algebra/Module/LinearMap/End.lean
+++ b/Mathlib/Algebra/Module/LinearMap/End.lean
@@ -6,6 +6,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
 -/
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.Module.LinearMap.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
 # Endomorphisms of a module
diff --git a/Mathlib/Algebra/Module/Pi.lean b/Mathlib/Algebra/Module/Pi.lean
index 1d6a967b8db91..23c86123bb947 100644
--- a/Mathlib/Algebra/Module/Pi.lean
+++ b/Mathlib/Algebra/Module/Pi.lean
@@ -83,17 +83,4 @@ instance module' {g : I → Type*} {r : ∀ i, Semiring (f i)} {m : ∀ i, AddCo
     -- Porting note: not sure why `apply zero_smul` fails here.
     rw [zero_smul]
 
-instance noZeroSMulDivisors (α) [Semiring α] [∀ i, AddCommMonoid <| f i]
-    [∀ i, Module α <| f i] [∀ i, NoZeroSMulDivisors α <| f i] :
-    NoZeroSMulDivisors α (∀ i : I, f i) :=
-  ⟨fun {_ _} h =>
-    or_iff_not_imp_left.mpr fun hc =>
-      funext fun i => (smul_eq_zero.mp (congr_fun h i)).resolve_left hc⟩
-
-/-- A special case of `Pi.noZeroSMulDivisors` for non-dependent types. Lean struggles to
-synthesize this instance by itself elsewhere in the library. -/
-instance _root_.Function.noZeroSMulDivisors {ι α β : Type*} [Semiring α] [AddCommMonoid β]
-    [Module α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (ι → β) :=
-  Pi.noZeroSMulDivisors _
-
 end Pi
diff --git a/Mathlib/Algebra/Module/Prod.lean b/Mathlib/Algebra/Module/Prod.lean
index 11b934777a06a..de41fcccad536 100644
--- a/Mathlib/Algebra/Module/Prod.lean
+++ b/Mathlib/Algebra/Module/Prod.lean
@@ -35,17 +35,4 @@ instance instModule [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M
     add_smul := fun _ _ _ => mk.inj_iff.mpr ⟨add_smul _ _ _, add_smul _ _ _⟩
     zero_smul := fun _ => mk.inj_iff.mpr ⟨zero_smul _ _, zero_smul _ _⟩ }
 
-instance noZeroSMulDivisors {r : Semiring R} [AddCommMonoid M] [AddCommMonoid N]
-    [Module R M] [Module R N] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] :
-    NoZeroSMulDivisors R (M × N) :=
-  { eq_zero_or_eq_zero_of_smul_eq_zero := by -- Porting note: in mathlib3 there is no need for `by`/
-      -- `intro`/`exact`, i.e. the following works:
-      -- ⟨fun c ⟨x, y⟩ h =>
-      --   or_iff_not_imp_left.mpr fun hc =>
-      intro c ⟨x, y⟩ h
-      exact or_iff_not_imp_left.mpr fun hc =>
-        mk.inj_iff.mpr
-          ⟨(smul_eq_zero.mp (congr_arg fst h)).resolve_left hc,
-            (smul_eq_zero.mp (congr_arg snd h)).resolve_left hc⟩ }
-
 end Prod
diff --git a/Mathlib/Algebra/Module/Rat.lean b/Mathlib/Algebra/Module/Rat.lean
index c0ed84a4366ed..3ce5e5ac011a8 100644
--- a/Mathlib/Algebra/Module/Rat.lean
+++ b/Mathlib/Algebra/Module/Rat.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Module.Basic
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Order.Field.Rat
 
diff --git a/Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean b/Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
new file mode 100644
index 0000000000000..f33114e9583a3
--- /dev/null
+++ b/Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Yury Kudryashov, Joseph Myers, Heather Macbeth, Kim Morrison, Yaël Dillies
+-/
+import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
+
+/-!
+# `NoZeroSMulDivisors`
+
+This file defines the `NoZeroSMulDivisors` class, and includes some tests
+for the vanishing of elements (especially in modules over division rings).
+-/
+
+assert_not_exists Multiset
+assert_not_exists Set.indicator
+assert_not_exists Pi.single_smul₀
+assert_not_exists Field
+
+section NoZeroSMulDivisors
+
+variable {R M : Type*}
+
+section Module
+
+section Nat
+
+theorem Nat.noZeroSMulDivisors
+    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] :
+    NoZeroSMulDivisors ℕ M where
+  eq_zero_or_eq_zero_of_smul_eq_zero {c x} := by rw [← Nat.cast_smul_eq_nsmul R, smul_eq_zero]; simp
+
+theorem two_nsmul_eq_zero
+    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : 2 • v = 0 ↔ v = 0 := by
+  haveI := Nat.noZeroSMulDivisors R M
+  simp [smul_eq_zero]
+
+end Nat
+
+variable [Semiring R]
+variable (R M)
+
+/-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
+zero as well. Usually `M` is an `R`-algebra. -/
+theorem CharZero.of_module (M) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R := by
+  refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩
+  rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
+
+end Module
+
+section AddCommGroup
+
+-- `R` can still be a semiring here
+variable [Semiring R] [AddCommGroup M] [Module R M]
+
+section SMulInjective
+
+variable (M)
+
+theorem smul_right_injective [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) :
+    Function.Injective (c • · : M → M) :=
+  (injective_iff_map_eq_zero (smulAddHom R M c)).2 fun _ ha => (smul_eq_zero.mp ha).resolve_left hc
+
+variable {M}
+
+theorem smul_right_inj [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M} :
+    c • x = c • y ↔ x = y :=
+  (smul_right_injective M hc).eq_iff
+
+end SMulInjective
+
+section Nat
+
+theorem self_eq_neg
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : v = -v ↔ v = 0 := by
+  rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]
+
+theorem neg_eq_self
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : -v = v ↔ v = 0 := by
+  rw [eq_comm, self_eq_neg R M]
+
+theorem self_ne_neg
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : v ≠ -v ↔ v ≠ 0 :=
+  (self_eq_neg R M).not
+
+theorem neg_ne_self
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : -v ≠ v ↔ v ≠ 0 :=
+  (neg_eq_self R M).not
+
+end Nat
+
+end AddCommGroup
+
+section Module
+
+variable [Ring R] [AddCommGroup M] [Module R M]
+
+section SMulInjective
+
+variable (R)
+variable [NoZeroSMulDivisors R M]
+
+theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x :=
+  fun c d h =>
+  sub_eq_zero.mp
+    ((smul_eq_zero.mp
+          (calc
+            (c - d) • x = c • x - d • x := sub_smul c d x
+            _ = 0 := sub_eq_zero.mpr h
+            )).resolve_right
+      hx)
+
+end SMulInjective
+
+instance [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
+  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩
+
+variable (R M)
+
+theorem NoZeroSMulDivisors.int_of_charZero
+    (R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] :
+    NoZeroSMulDivisors ℤ M :=
+  ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩
+
+/-- Only a ring of characteristic zero can have a non-trivial module without additive or
+scalar torsion. -/
+theorem CharZero.of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R := by
+  refine ⟨fun {n m h} ↦ ?_⟩
+  obtain ⟨x, hx⟩ := exists_ne (0 : M)
+  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
+  simpa using smul_left_injective ℤ hx h
+
+instance [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
+  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ c x, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩
+
+end Module
+
+section GroupWithZero
+
+variable [GroupWithZero R] [AddMonoid M] [DistribMulAction R M]
+
+-- see note [lower instance priority]
+/-- This instance applies to `DivisionSemiring`s, in particular `NNReal` and `NNRat`. -/
+instance (priority := 100) GroupWithZero.toNoZeroSMulDivisors : NoZeroSMulDivisors R M :=
+  ⟨fun {a _} h ↦ or_iff_not_imp_left.2 fun ha ↦ (smul_eq_zero_iff_eq <| Units.mk0 a ha).1 h⟩
+
+end GroupWithZero
+
+end NoZeroSMulDivisors
diff --git a/Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean b/Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
new file mode 100644
index 0000000000000..caa70e20f08e3
--- /dev/null
+++ b/Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Yury Kudryashov, Joseph Myers, Heather Macbeth, Kim Morrison, Yaël Dillies
+-/
+import Mathlib.Algebra.SMulWithZero
+
+/-!
+# `NoZeroSMulDivisors`
+
+This file defines the `NoZeroSMulDivisors` class, and includes some tests
+for the vanishing of elements (especially in modules over division rings).
+-/
+
+assert_not_exists Multiset
+assert_not_exists Set.indicator
+assert_not_exists Pi.single_smul₀
+assert_not_exists Field
+assert_not_exists Module
+
+section NoZeroSMulDivisors
+
+/-! ### `NoZeroSMulDivisors`
+
+-/
+
+variable {R M : Type*}
+
+/-- `NoZeroSMulDivisors R M` states that a scalar multiple is `0` only if either argument is `0`.
+This is a version of saying that `M` is torsion free, without assuming `R` is zero-divisor free.
+
+The main application of `NoZeroSMulDivisors R M`, when `M` is a module,
+is the result `smul_eq_zero`: a scalar multiple is `0` iff either argument is `0`.
+
+It is a generalization of the `NoZeroDivisors` class to heterogeneous multiplication.
+-/
+@[mk_iff]
+class NoZeroSMulDivisors (R M : Type*) [Zero R] [Zero M] [SMul R M] : Prop where
+  /-- If scalar multiplication yields zero, either the scalar or the vector was zero. -/
+  eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0
+
+export NoZeroSMulDivisors (eq_zero_or_eq_zero_of_smul_eq_zero)
+
+/-- Pullback a `NoZeroSMulDivisors` instance along an injective function. -/
+theorem Function.Injective.noZeroSMulDivisors {R M N : Type*} [Zero R] [Zero M] [Zero N]
+    [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.Injective f)
+    (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M :=
+  ⟨fun {_ _} h =>
+    Or.imp_right (@hf _ _) <| h0.symm ▸ eq_zero_or_eq_zero_of_smul_eq_zero (by rw [← hs, h, h0])⟩
+
+-- See note [lower instance priority]
+instance (priority := 100) NoZeroDivisors.toNoZeroSMulDivisors [Zero R] [Mul R]
+    [NoZeroDivisors R] : NoZeroSMulDivisors R R :=
+  ⟨fun {_ _} => eq_zero_or_eq_zero_of_mul_eq_zero⟩
+
+theorem smul_ne_zero [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M}
+    (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0 := fun h =>
+  (eq_zero_or_eq_zero_of_smul_eq_zero h).elim hc hx
+
+section SMulWithZero
+
+variable [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M}
+
+@[simp]
+theorem smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=
+  ⟨eq_zero_or_eq_zero_of_smul_eq_zero, fun h =>
+    h.elim (fun h => h.symm ▸ zero_smul R x) fun h => h.symm ▸ smul_zero c⟩
+
+theorem smul_ne_zero_iff : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 := by rw [Ne, smul_eq_zero, not_or]
+
+lemma smul_eq_zero_iff_left (hx : x ≠ 0) : c • x = 0 ↔ c = 0 := by simp [hx]
+lemma smul_eq_zero_iff_right (hc : c ≠ 0) : c • x = 0 ↔ x = 0 := by simp [hc]
+lemma smul_ne_zero_iff_left (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0 := by simp [hx]
+lemma smul_ne_zero_iff_right (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0 := by simp [hc]
+
+end SMulWithZero
+
+end NoZeroSMulDivisors
diff --git a/Mathlib/Algebra/NoZeroSMulDivisors/Pi.lean b/Mathlib/Algebra/NoZeroSMulDivisors/Pi.lean
new file mode 100644
index 0000000000000..ac7b42a019040
--- /dev/null
+++ b/Mathlib/Algebra/NoZeroSMulDivisors/Pi.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Yaël Dillies
+-/
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
+import Mathlib.Algebra.Group.Action.Pi
+
+/-!
+# Pi instances for NoZeroSMulDivisors
+
+This file defines instances for NoZeroSMulDivisors on Pi types.
+-/
+
+
+universe u v
+
+variable {I : Type u}
+
+-- The indexing type
+variable {f : I → Type v}
+
+instance Pi.noZeroSMulDivisors (α) [Zero α] [∀ i, Zero <| f i]
+    [∀ i, SMulWithZero α <| f i] [∀ i, NoZeroSMulDivisors α <| f i] :
+    NoZeroSMulDivisors α (∀ i : I, f i) :=
+  ⟨fun {_ _} h =>
+    or_iff_not_imp_left.mpr fun hc =>
+      funext fun i => (smul_eq_zero.mp (congr_fun h i)).resolve_left hc⟩
+
+/-- A special case of `Pi.noZeroSMulDivisors` for non-dependent types. Lean struggles to
+synthesize this instance by itself elsewhere in the library. -/
+instance _root_.Function.noZeroSMulDivisors {ι α β : Type*} [Zero α] [Zero β]
+    [SMulWithZero α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (ι → β) :=
+  Pi.noZeroSMulDivisors _
diff --git a/Mathlib/Algebra/NoZeroSMulDivisors/Prod.lean b/Mathlib/Algebra/NoZeroSMulDivisors/Prod.lean
new file mode 100644
index 0000000000000..e836979c0377a
--- /dev/null
+++ b/Mathlib/Algebra/NoZeroSMulDivisors/Prod.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
+import Mathlib.Algebra.Group.Action.Prod
+
+/-!
+# Prod instances for NoZeroSMulDivisors
+
+This file defines a NoZeroSMulDivisors instance for the binary product of actions.
+-/
+
+variable {R M N : Type*}
+
+namespace Prod
+
+instance noZeroSMulDivisors [Zero R] [Zero M] [Zero N]
+    [SMulWithZero R M] [SMulWithZero R N] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] :
+    NoZeroSMulDivisors R (M × N) :=
+  { eq_zero_or_eq_zero_of_smul_eq_zero := by -- Porting note: in mathlib3 there is no need for `by`/
+      -- `intro`/`exact`, i.e. the following works:
+      -- ⟨fun c ⟨x, y⟩ h =>
+      --   or_iff_not_imp_left.mpr fun hc =>
+      intro c ⟨x, y⟩ h
+      exact or_iff_not_imp_left.mpr fun hc =>
+        mk.inj_iff.mpr
+          ⟨(smul_eq_zero.mp (congr_arg fst h)).resolve_left hc,
+            (smul_eq_zero.mp (congr_arg snd h)).resolve_left hc⟩ }
+
+end Prod
diff --git a/Mathlib/Algebra/Notation.lean b/Mathlib/Algebra/Notation.lean
index 0ea472b668eb9..ffb3097c7ba73 100644
--- a/Mathlib/Algebra/Notation.lean
+++ b/Mathlib/Algebra/Notation.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
+import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.ToAdditive
 
 /-!
diff --git a/Mathlib/Algebra/Order/AbsoluteValue.lean b/Mathlib/Algebra/Order/AbsoluteValue.lean
index 0dcc6acdcfbb4..fae16b0ffcd6d 100644
--- a/Mathlib/Algebra/Order/AbsoluteValue.lean
+++ b/Mathlib/Algebra/Order/AbsoluteValue.lean
@@ -77,11 +77,6 @@ def Simps.apply (f : AbsoluteValue R S) : R → S :=
 
 initialize_simps_projections AbsoluteValue (toMulHom_toFun → apply)
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.has_coe_to_fun`
-directly. -/
-instance : CoeFun (AbsoluteValue R S) fun _ => R → S :=
-  DFunLike.hasCoeToFun
-
 @[simp]
 theorem coe_toMulHom : ⇑abv.toMulHom = abv :=
   rfl
diff --git a/Mathlib/Algebra/Order/Module/Defs.lean b/Mathlib/Algebra/Order/Module/Defs.lean
index 8323669b29434..a1172e5a8524d 100644
--- a/Mathlib/Algebra/Order/Module/Defs.lean
+++ b/Mathlib/Algebra/Order/Module/Defs.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
 import Mathlib.Tactic.GCongr
diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean
index 6370c2c91944e..6df890e8638a3 100644
--- a/Mathlib/Algebra/Order/Star/Basic.lean
+++ b/Mathlib/Algebra/Order/Star/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Star.SelfAdjoint
diff --git a/Mathlib/Algebra/Ring/CentroidHom.lean b/Mathlib/Algebra/Ring/CentroidHom.lean
index 37a70431efb16..b1b90bb34b9d1 100644
--- a/Mathlib/Algebra/Ring/CentroidHom.lean
+++ b/Mathlib/Algebra/Ring/CentroidHom.lean
@@ -102,13 +102,6 @@ instance : CentroidHomClass (CentroidHom α) α where
   map_mul_right f := f.map_mul_right'
 
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.CoeFun`
-directly. -/
-/- Porting note: Lean gave me `unknown constant 'DFunLike.CoeFun'` and says `CoeFun` is a type
-mismatch, so I used `library_search`. -/
-instance : CoeFun (CentroidHom α) fun _ ↦ α → α :=
-  inferInstanceAs (CoeFun (CentroidHom α) fun _ ↦ α → α)
-
 -- Porting note: removed @[simp]; not in normal form. (`toAddMonoidHom_eq_coe` below ensures that
 -- the LHS simplifies to the RHS anyway.)
 theorem toFun_eq_coe {f : CentroidHom α} : f.toFun = f := rfl
diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean
index e4257988bc45b..55726f263e5bf 100644
--- a/Mathlib/Analysis/Complex/Basic.lean
+++ b/Mathlib/Analysis/Complex/Basic.lean
@@ -598,10 +598,10 @@ theorem ofReal_tsum (f : α → ℝ) : (↑(∑' a, f a) : ℂ) = ∑' a, ↑(f
   RCLike.ofReal_tsum _ _
 
 theorem hasSum_re {f : α → ℂ} {x : ℂ} (h : HasSum f x) : HasSum (fun x => (f x).re) x.re :=
-  RCLike.hasSum_re _ h
+  RCLike.hasSum_re ℂ h
 
 theorem hasSum_im {f : α → ℂ} {x : ℂ} (h : HasSum f x) : HasSum (fun x => (f x).im) x.im :=
-  RCLike.hasSum_im _ h
+  RCLike.hasSum_im ℂ h
 
 theorem re_tsum {f : α → ℂ} (h : Summable f) : (∑' a, f a).re = ∑' a, (f a).re :=
   RCLike.re_tsum _ h
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
index ba8aae073aff9..a9cd6e02b3fbe 100644
--- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean
+++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
@@ -90,10 +90,6 @@ instance instFunLike : FunLike 𝓢(E, F) E F where
   coe f := f.toFun
   coe_injective' f g h := by cases f; cases g; congr
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-instance instCoeFun : CoeFun 𝓢(E, F) fun _ => E → F :=
-  DFunLike.hasCoeToFun
-
 /-- All derivatives of a Schwartz function are rapidly decaying. -/
 theorem decay (f : 𝓢(E, F)) (k n : ℕ) :
     ∃ C : ℝ, 0 < C ∧ ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C := by
diff --git a/Mathlib/Analysis/Normed/Algebra/Norm.lean b/Mathlib/Analysis/Normed/Algebra/Norm.lean
index eb815ac91298e..715ad8694cf6f 100644
--- a/Mathlib/Analysis/Normed/Algebra/Norm.lean
+++ b/Mathlib/Analysis/Normed/Algebra/Norm.lean
@@ -70,10 +70,6 @@ instance algebraNormClass : AlgebraNormClass (AlgebraNorm R S) R S where
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
   map_smul_eq_mul f := f.smul'
 
-/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`. -/
-instance : CoeFun (AlgebraNorm R S) fun _ => S → ℝ :=
-  DFunLike.hasCoeToFun
-
 theorem toFun_eq_coe (p : AlgebraNorm R S) : p.toFun = p := rfl
 
 @[ext]
@@ -160,10 +156,6 @@ instance mulAlgebraNormClass : MulAlgebraNormClass (MulAlgebraNorm R S) R S wher
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
   map_smul_eq_mul f := f.smul'
 
-/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`. -/
-instance : CoeFun (MulAlgebraNorm R S) fun _ => S → ℝ :=
-  DFunLike.hasCoeToFun
-
 theorem toFun_eq_coe (p : MulAlgebraNorm R S) : p.toFun = p := rfl
 
 @[ext]
diff --git a/Mathlib/Analysis/Normed/Group/Seminorm.lean b/Mathlib/Analysis/Normed/Group/Seminorm.lean
index eede911fb046d..a8d9220ba89cc 100644
--- a/Mathlib/Analysis/Normed/Group/Seminorm.lean
+++ b/Mathlib/Analysis/Normed/Group/Seminorm.lean
@@ -181,12 +181,6 @@ instance groupSeminormClass : GroupSeminormClass (GroupSeminorm E) E ℝ where
   map_mul_le_add f := f.mul_le'
   map_inv_eq_map f := f.inv'
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-@[to_additive "Helper instance for when there's too many metavariables to apply
-`DFunLike.hasCoeToFun`. "]
-instance : CoeFun (GroupSeminorm E) fun _ => E → ℝ :=
-  ⟨DFunLike.coe⟩
-
 @[to_additive (attr := simp)]
 theorem toFun_eq_coe : p.toFun = p :=
   rfl
@@ -447,10 +441,6 @@ instance nonarchAddGroupSeminormClass :
   map_zero f := f.map_zero'
   map_neg_eq_map' f := f.neg'
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-instance : CoeFun (NonarchAddGroupSeminorm E) fun _ => E → ℝ :=
-  ⟨DFunLike.coe⟩
-
 -- Porting note: `simpNF` said the left hand side simplified to this
 @[simp]
 theorem toZeroHom_eq_coe : ⇑p.toZeroHom = p := by
@@ -667,13 +657,6 @@ instance groupNormClass : GroupNormClass (GroupNorm E) E ℝ where
   map_inv_eq_map f := f.inv'
   eq_one_of_map_eq_zero f := f.eq_one_of_map_eq_zero' _
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`
-directly. -/
-@[to_additive "Helper instance for when there's too many metavariables to apply
-`DFunLike.hasCoeToFun` directly. "]
-instance : CoeFun (GroupNorm E) fun _ => E → ℝ :=
-  DFunLike.hasCoeToFun
-
 -- Porting note: `simpNF` told me the left-hand side simplified to this
 @[to_additive (attr := simp)]
 theorem toGroupSeminorm_eq_coe : ⇑p.toGroupSeminorm = p :=
@@ -799,10 +782,6 @@ instance nonarchAddGroupNormClass : NonarchAddGroupNormClass (NonarchAddGroupNor
   map_neg_eq_map' f := f.neg'
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-noncomputable instance : CoeFun (NonarchAddGroupNorm E) fun _ => E → ℝ :=
-  DFunLike.hasCoeToFun
-
 -- Porting note: `simpNF` told me the left-hand side simplified to this
 @[simp]
 theorem toNonarchAddGroupSeminorm_eq_coe : ⇑p.toNonarchAddGroupSeminorm = p :=
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean b/Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean
index e501871d0f757..a4e8274b8176e 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean
@@ -75,7 +75,7 @@ variable {G : Type v} [Group G] (J : SingleObj G ⥤ Type u)
 equivalent to the `MulAction.orbitRel` equivalence relation on `J.obj (SingleObj.star G)`. -/
 lemma Types.Quot.Rel.iff_orbitRel (x y : J.obj (SingleObj.star G)) :
     Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩
-    ↔ Setoid.Rel (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y := by
+    ↔ MulAction.orbitRel G (J.obj (SingleObj.star G)) x y := by
   have h (g : G) : y = g • x ↔ g • x = y := ⟨symm, symm⟩
   conv => rhs; rw [Setoid.comm']
   show (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)
diff --git a/Mathlib/Data/ENNReal/Operations.lean b/Mathlib/Data/ENNReal/Operations.lean
index 473c3d6c65d78..26c974025ccf6 100644
--- a/Mathlib/Data/ENNReal/Operations.lean
+++ b/Mathlib/Data/ENNReal/Operations.lean
@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.WithTop
 import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Module.Basic
 import Mathlib.Data.ENNReal.Basic
 
 /-!
diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean
index a11fa73582072..2bec860ba95b9 100644
--- a/Mathlib/Data/Quot.lean
+++ b/Mathlib/Data/Quot.lean
@@ -26,6 +26,8 @@ run_cmd Lean.Elab.Command.liftTermElabM do
   Lean.Meta.registerCoercion ``Setoid.r
     (some { numArgs := 2, coercee := 1, type := .coeFun })
 
+/-- When writing a lemma about `someSetoid x y` (which uses this instance),
+call it `someSetoid_apply` not `someSetoid_r`. -/
 instance : CoeFun (Setoid α) (fun _ ↦ α → α → Prop) where
   coe := @Setoid.r _
 
diff --git a/Mathlib/Data/Set/Pointwise/SMul.lean b/Mathlib/Data/Set/Pointwise/SMul.lean
index 9e6917fe0172c..bd562b3fb02ad 100644
--- a/Mathlib/Data/Set/Pointwise/SMul.lean
+++ b/Mathlib/Data/Set/Pointwise/SMul.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Group.Pi.Basic
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.GroupWithZero.Action.Basic
 import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 import Mathlib.Data.Set.Pairwise.Basic
 
 /-!
diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean
index c34439b36e1e1..e4b60325f1b21 100644
--- a/Mathlib/Data/Setoid/Basic.lean
+++ b/Mathlib/Data/Setoid/Basic.lean
@@ -15,9 +15,6 @@ theorems for quotients of arbitrary types.
 
 ## Implementation notes
 
-The function `Rel` and lemmas ending in ' make it easier to talk about different
-equivalence relations on the same type.
-
 The complete lattice instance for equivalence relations could have been defined by lifting
 the Galois insertion of equivalence relations on α into binary relations on α, and then using
 `CompleteLattice.copy` to define a complete lattice instance with more appropriate
@@ -39,47 +36,57 @@ attribute [trans] Setoid.trans
 variable {α : Type*} {β : Type*}
 
 /-- A version of `Setoid.r` that takes the equivalence relation as an explicit argument. -/
+@[deprecated (since := "2024-08-29")]
 def Setoid.Rel (r : Setoid α) : α → α → Prop :=
   @Setoid.r _ r
 
+set_option linter.deprecated false in
+@[deprecated (since := "2024-10-09")]
 instance Setoid.decidableRel (r : Setoid α) [h : DecidableRel r.r] : DecidableRel r.Rel :=
   h
 
+set_option linter.deprecated false in
 /-- A version of `Quotient.eq'` compatible with `Setoid.Rel`, to make rewriting possible. -/
+@[deprecated Quotient.eq' (since := "2024-10-09")]
 theorem Quotient.eq_rel {r : Setoid α} {x y} :
     (Quotient.mk' x : Quotient r) = Quotient.mk' y ↔ r.Rel x y :=
   Quotient.eq
 
 namespace Setoid
 
-@[ext]
+attribute [ext] ext
+
+set_option linter.deprecated false in
+@[deprecated Setoid.ext (since := "2024-10-09")]
 theorem ext' {r s : Setoid α} (H : ∀ a b, r.Rel a b ↔ s.Rel a b) : r = s :=
   ext H
 
-theorem ext_iff {r s : Setoid α} : r = s ↔ ∀ a b, r.Rel a b ↔ s.Rel a b :=
+set_option linter.deprecated false in
+@[deprecated Setoid.ext_iff (since := "2024-10-09")]
+theorem ext'_iff {r s : Setoid α} : r = s ↔ ∀ a b, r.Rel a b ↔ s.Rel a b :=
   ⟨fun h _ _ => h ▸ Iff.rfl, ext'⟩
 
 /-- Two equivalence relations are equal iff their underlying binary operations are equal. -/
-theorem eq_iff_rel_eq {r₁ r₂ : Setoid α} : r₁ = r₂ ↔ r₁.Rel = r₂.Rel :=
-  ⟨fun h => h ▸ rfl, fun h => Setoid.ext' fun _ _ => h ▸ Iff.rfl⟩
+theorem eq_iff_rel_eq {r₁ r₂ : Setoid α} : r₁ = r₂ ↔ ⇑r₁ = ⇑r₂ :=
+  ⟨fun h => h ▸ rfl, fun h => Setoid.ext fun _ _ => h ▸ Iff.rfl⟩
 
 /-- Defining `≤` for equivalence relations. -/
 instance : LE (Setoid α) :=
-  ⟨fun r s => ∀ ⦃x y⦄, r.Rel x y → s.Rel x y⟩
+  ⟨fun r s => ∀ ⦃x y⦄, r x y → s x y⟩
 
-theorem le_def {r s : Setoid α} : r ≤ s ↔ ∀ {x y}, r.Rel x y → s.Rel x y :=
+theorem le_def {r s : Setoid α} : r ≤ s ↔ ∀ {x y}, r x y → s x y :=
   Iff.rfl
 
 @[refl]
-theorem refl' (r : Setoid α) (x) : r.Rel x x := r.iseqv.refl x
+theorem refl' (r : Setoid α) (x) : r x x := r.iseqv.refl x
 
 @[symm]
-theorem symm' (r : Setoid α) : ∀ {x y}, r.Rel x y → r.Rel y x := r.iseqv.symm
+theorem symm' (r : Setoid α) : ∀ {x y}, r x y → r y x := r.iseqv.symm
 
 @[trans]
-theorem trans' (r : Setoid α) : ∀ {x y z}, r.Rel x y → r.Rel y z → r.Rel x z := r.iseqv.trans
+theorem trans' (r : Setoid α) : ∀ {x y z}, r x y → r y z → r x z := r.iseqv.trans
 
-theorem comm' (s : Setoid α) {x y} : s.Rel x y ↔ s.Rel y x :=
+theorem comm' (s : Setoid α) {x y} : s x y ↔ s y x :=
   ⟨s.symm', s.symm'⟩
 
 /-- The kernel of a function is an equivalence relation. -/
@@ -89,7 +96,7 @@ def ker (f : α → β) : Setoid α :=
 /-- The kernel of the quotient map induced by an equivalence relation r equals r. -/
 @[simp]
 theorem ker_mk_eq (r : Setoid α) : ker (@Quotient.mk'' _ r) = r :=
-  ext' fun _ _ => Quotient.eq
+  ext fun _ _ => Quotient.eq
 
 theorem ker_apply_mk_out {f : α → β} (a : α) : f (⟦a⟧ : Quotient (Setoid.ker f)).out = f a :=
   @Quotient.mk_out _ (Setoid.ker f) a
@@ -98,7 +105,7 @@ theorem ker_apply_mk_out' {f : α → β} (a : α) :
     f (Quotient.mk _ a : Quotient <| Setoid.ker f).out' = f a :=
   @Quotient.mk_out' _ (Setoid.ker f) a
 
-theorem ker_def {f : α → β} {x y : α} : (ker f).Rel x y ↔ f x = f y :=
+theorem ker_def {f : α → β} {x y : α} : ker f x y ↔ f x = f y :=
   Iff.rfl
 
 /-- Given types `α`, `β`, the product of two equivalence relations `r` on `α` and `s` on `β`:
@@ -106,7 +113,7 @@ theorem ker_def {f : α → β} {x y : α} : (ker f).Rel x y ↔ f x = f y :=
     by `r` and `x₂` is related to `y₂` by `s`. -/
 protected def prod (r : Setoid α) (s : Setoid β) :
     Setoid (α × β) where
-  r x y := r.Rel x.1 y.1 ∧ s.Rel x.2 y.2
+  r x y := r x.1 y.1 ∧ s x.2 y.2
   iseqv :=
     ⟨fun x => ⟨r.refl' x.1, s.refl' x.2⟩, fun h => ⟨r.symm' h.1, s.symm' h.2⟩,
       fun h₁ h₂ => ⟨r.trans' h₁.1 h₂.1, s.trans' h₁.2 h₂.2⟩⟩
@@ -157,28 +164,28 @@ noncomputable def piQuotientEquiv {ι : Sort*} {α : ι → Sort*} (r : ∀ i, S
 /-- The infimum of two equivalence relations. -/
 instance : Inf (Setoid α) :=
   ⟨fun r s =>
-    ⟨fun x y => r.Rel x y ∧ s.Rel x y,
+    ⟨fun x y => r x y ∧ s x y,
       ⟨fun x => ⟨r.refl' x, s.refl' x⟩, fun h => ⟨r.symm' h.1, s.symm' h.2⟩, fun h1 h2 =>
         ⟨r.trans' h1.1 h2.1, s.trans' h1.2 h2.2⟩⟩⟩⟩
 
 /-- The infimum of 2 equivalence relations r and s is the same relation as the infimum
     of the underlying binary operations. -/
-theorem inf_def {r s : Setoid α} : (r ⊓ s).Rel = r.Rel ⊓ s.Rel :=
+theorem inf_def {r s : Setoid α} : ⇑(r ⊓ s) = ⇑r ⊓ ⇑s :=
   rfl
 
-theorem inf_iff_and {r s : Setoid α} {x y} : (r ⊓ s).Rel x y ↔ r.Rel x y ∧ s.Rel x y :=
+theorem inf_iff_and {r s : Setoid α} {x y} : (r ⊓ s) x y ↔ r x y ∧ s x y :=
   Iff.rfl
 
 /-- The infimum of a set of equivalence relations. -/
 instance : InfSet (Setoid α) :=
   ⟨fun S =>
-    { r := fun x y => ∀ r ∈ S, r.Rel x y
+    { r := fun x y => ∀ r ∈ S, r x y
       iseqv := ⟨fun x r _ => r.refl' x, fun h r hr => r.symm' <| h r hr, fun h1 h2 r hr =>
         r.trans' (h1 r hr) <| h2 r hr⟩ }⟩
 
 /-- The underlying binary operation of the infimum of a set of equivalence relations
     is the infimum of the set's image under the map to the underlying binary operation. -/
-theorem sInf_def {s : Set (Setoid α)} : (sInf s).Rel = sInf (Rel '' s) := by
+theorem sInf_def {s : Set (Setoid α)} : ⇑(sInf s) = sInf ((⇑) '' s) := by
   ext
   simp only [sInf_image, iInf_apply, iInf_Prop_eq]
   rfl
@@ -189,7 +196,7 @@ instance : PartialOrder (Setoid α) where
   le_refl _ _ _ := id
   le_trans _ _ _ hr hs _ _ h := hs <| hr h
   lt_iff_le_not_le _ _ := Iff.rfl
-  le_antisymm _ _ h1 h2 := Setoid.ext' fun _ _ => ⟨fun h => h1 h, fun h => h2 h⟩
+  le_antisymm _ _ h1 h2 := Setoid.ext fun _ _ => ⟨fun h => h1 h, fun h => h2 h⟩
 
 /-- The complete lattice of equivalence relations on a type, with bottom element `=`
     and top element the trivial equivalence relation. -/
@@ -206,20 +213,20 @@ instance completeLattice : CompleteLattice (Setoid α) :=
     bot_le := fun r x _ h => h ▸ r.2.1 x }
 
 @[simp]
-theorem top_def : (⊤ : Setoid α).Rel = ⊤ :=
+theorem top_def : ⇑(⊤ : Setoid α) = ⊤ :=
   rfl
 
 @[simp]
-theorem bot_def : (⊥ : Setoid α).Rel = (· = ·) :=
+theorem bot_def : ⇑(⊥ : Setoid α) = (· = ·) :=
   rfl
 
-theorem eq_top_iff {s : Setoid α} : s = (⊤ : Setoid α) ↔ ∀ x y : α, s.Rel x y := by
+theorem eq_top_iff {s : Setoid α} : s = (⊤ : Setoid α) ↔ ∀ x y : α, s x y := by
   rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]
   simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]
 
 lemma sInf_equiv {S : Set (Setoid α)} {x y : α} :
     letI := sInf S
-    x ≈ y ↔ ∀ s ∈ S, s.Rel x y := Iff.rfl
+    x ≈ y ↔ ∀ s ∈ S, s x y := Iff.rfl
 
 lemma sInf_iff {S : Set (Setoid α)} {x y : α} :
     sInf S x y ↔ ∀ s ∈ S, s x y := Iff.rfl
@@ -245,7 +252,7 @@ open Relation
 /-- The inductively defined equivalence closure of a binary relation r is the infimum
     of the set of all equivalence relations containing r. -/
 theorem eqvGen_eq (r : α → α → Prop) :
-    EqvGen.setoid r = sInf { s : Setoid α | ∀ ⦃x y⦄, r x y → s.Rel x y } :=
+    EqvGen.setoid r = sInf { s : Setoid α | ∀ ⦃x y⦄, r x y → s x y } :=
   le_antisymm
     (fun _ _ H =>
       EqvGen.rec (fun _ _ h _ hs => hs h) (refl' _) (fun _ _ _ => symm' _)
@@ -255,20 +262,20 @@ theorem eqvGen_eq (r : α → α → Prop) :
 /-- The supremum of two equivalence relations r and s is the equivalence closure of the binary
     relation `x is related to y by r or s`. -/
 theorem sup_eq_eqvGen (r s : Setoid α) :
-    r ⊔ s = EqvGen.setoid fun x y => r.Rel x y ∨ s.Rel x y := by
+    r ⊔ s = EqvGen.setoid fun x y => r x y ∨ s x y := by
   rw [eqvGen_eq]
   apply congr_arg sInf
   simp only [le_def, or_imp, ← forall_and]
 
 /-- The supremum of 2 equivalence relations r and s is the equivalence closure of the
     supremum of the underlying binary operations. -/
-theorem sup_def {r s : Setoid α} : r ⊔ s = EqvGen.setoid (r.Rel ⊔ s.Rel) := by
+theorem sup_def {r s : Setoid α} : r ⊔ s = EqvGen.setoid (⇑r ⊔ ⇑s) := by
   rw [sup_eq_eqvGen]; rfl
 
 /-- The supremum of a set S of equivalence relations is the equivalence closure of the binary
     relation `there exists r ∈ S relating x and y`. -/
 theorem sSup_eq_eqvGen (S : Set (Setoid α)) :
-    sSup S = EqvGen.setoid fun x y => ∃ r : Setoid α, r ∈ S ∧ r.Rel x y := by
+    sSup S = EqvGen.setoid fun x y => ∃ r : Setoid α, r ∈ S ∧ r x y := by
   rw [eqvGen_eq]
   apply congr_arg sInf
   simp only [upperBounds, le_def, and_imp, exists_imp]
@@ -277,7 +284,7 @@ theorem sSup_eq_eqvGen (S : Set (Setoid α)) :
 
 /-- The supremum of a set of equivalence relations is the equivalence closure of the
     supremum of the set's image under the map to the underlying binary operation. -/
-theorem sSup_def {s : Set (Setoid α)} : sSup s = EqvGen.setoid (sSup (Rel '' s)) := by
+theorem sSup_def {s : Set (Setoid α)} : sSup s = EqvGen.setoid (sSup ((⇑) '' s)) := by
   rw [sSup_eq_eqvGen, sSup_image]
   congr with (x y)
   simp only [iSup_apply, iSup_Prop_eq, exists_prop]
@@ -288,13 +295,12 @@ theorem eqvGen_of_setoid (r : Setoid α) : EqvGen.setoid r.r = r :=
   le_antisymm (by rw [eqvGen_eq]; exact sInf_le fun _ _ => id) EqvGen.rel
 
 /-- Equivalence closure is idempotent. -/
-@[simp]
-theorem eqvGen_idem (r : α → α → Prop) : EqvGen.setoid (EqvGen.setoid r).Rel = EqvGen.setoid r :=
+theorem eqvGen_idem (r : α → α → Prop) : EqvGen.setoid (EqvGen.setoid r) = EqvGen.setoid r :=
   eqvGen_of_setoid _
 
 /-- The equivalence closure of a binary relation r is contained in any equivalence
     relation containing r. -/
-theorem eqvGen_le {r : α → α → Prop} {s : Setoid α} (h : ∀ x y, r x y → s.Rel x y) :
+theorem eqvGen_le {r : α → α → Prop} {s : Setoid α} (h : ∀ x y, r x y → s x y) :
     EqvGen.setoid r ≤ s := by rw [eqvGen_eq]; exact sInf_le h
 
 /-- Equivalence closure of binary relations is monotone. -/
@@ -304,7 +310,7 @@ theorem eqvGen_mono {r s : α → α → Prop} (h : ∀ x y, r x y → s x y) :
 
 /-- There is a Galois insertion of equivalence relations on α into binary relations
     on α, with equivalence closure the lower adjoint. -/
-def gi : @GaloisInsertion (α → α → Prop) (Setoid α) _ _ EqvGen.setoid Rel where
+def gi : @GaloisInsertion (α → α → Prop) (Setoid α) _ _ EqvGen.setoid (⇑) where
   choice r _ := EqvGen.setoid r
   gc _ s := ⟨fun H _ _ h => H <| EqvGen.rel _ _ h, fun H => eqvGen_of_setoid s ▸ eqvGen_mono H⟩
   le_l_u x := (eqvGen_of_setoid x).symm ▸ le_refl x
@@ -320,7 +326,7 @@ theorem injective_iff_ker_bot (f : α → β) : Injective f ↔ ker f = ⊥ :=
   (@eq_bot_iff (Setoid α) _ _ (ker f)).symm
 
 /-- The elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f. -/
-theorem ker_iff_mem_preimage {f : α → β} {x y} : (ker f).Rel x y ↔ x ∈ f ⁻¹' {f y} :=
+theorem ker_iff_mem_preimage {f : α → β} {x y} : ker f x y ↔ x ∈ f ⁻¹' {f y} :=
   Iff.rfl
 
 /-- Equivalence between functions `α → β` such that `r x y → f x = f y` and functions
@@ -345,7 +351,7 @@ theorem ker_lift_injective (f : α → β) : Injective (@Quotient.lift _ _ (ker
 
 /-- Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose
     induced map from the quotient of α to β is injective. -/
-theorem ker_eq_lift_of_injective {r : Setoid α} (f : α → β) (H : ∀ x y, r.Rel x y → f x = f y)
+theorem ker_eq_lift_of_injective {r : Setoid α} (f : α → β) (H : ∀ x y, r x y → f x = f y)
     (h : Injective (Quotient.lift f H)) : ker f = r :=
   le_antisymm
     (fun x y hk =>
@@ -387,13 +393,13 @@ variable {r f}
     closure of the relation on `f`'s image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are
     related to the elements of `f⁻¹(y)` by `r`.' -/
 def map (r : Setoid α) (f : α → β) : Setoid β :=
-  Relation.EqvGen.setoid fun x y => ∃ a b, f a = x ∧ f b = y ∧ r.Rel a b
+  Relation.EqvGen.setoid fun x y => ∃ a b, f a = x ∧ f b = y ∧ r a b
 
 /-- Given a surjective function f whose kernel is contained in an equivalence relation r, the
     equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to
     the elements of f⁻¹(y) by r. -/
 def mapOfSurjective (r) (f : α → β) (h : ker f ≤ r) (hf : Surjective f) : Setoid β :=
-  ⟨fun x y => ∃ a b, f a = x ∧ f b = y ∧ r.Rel a b,
+  ⟨fun x y => ∃ a b, f a = x ∧ f b = y ∧ r a b,
     ⟨fun x =>
       let ⟨y, hy⟩ := hf x
       ⟨y, y, hy, hy, r.refl' y⟩,
@@ -411,9 +417,9 @@ relation on `α` defined by '`x ≈ y` iff `f(x)` is related to `f(y)` by `r`'.
 
 See note [reducible non-instances]. -/
 abbrev comap (f : α → β) (r : Setoid β) : Setoid α :=
-  ⟨r.Rel on f, r.iseqv.comap _⟩
+  ⟨r on f, r.iseqv.comap _⟩
 
-theorem comap_rel (f : α → β) (r : Setoid β) (x y : α) : (comap f r).Rel x y ↔ r.Rel (f x) (f y) :=
+theorem comap_rel (f : α → β) (r : Setoid β) (x y : α) : comap f r x y ↔ r (f x) (f y) :=
   Iff.rfl
 
 /-- Given a map `f : N → M` and an equivalence relation `r` on `β`, the equivalence relation
@@ -424,7 +430,8 @@ theorem comap_eq {f : α → β} {r : Setoid β} : comap f r = ker (@Quotient.mk
 /-- The second isomorphism theorem for sets. -/
 noncomputable def comapQuotientEquiv (f : α → β) (r : Setoid β) :
     Quotient (comap f r) ≃ Set.range (@Quotient.mk'' _ r ∘ f) :=
-  (Quotient.congrRight <| ext_iff.1 comap_eq).trans <| quotientKerEquivRange <| Quotient.mk'' ∘ f
+  (Quotient.congrRight <| Setoid.ext_iff.1 comap_eq).trans <| quotientKerEquivRange <|
+    Quotient.mk'' ∘ f
 
 variable (r f)
 
@@ -454,7 +461,7 @@ def correspondence (r : Setoid α) : { s // r ≤ s } ≃o Setoid (Quotient r) w
       (fun h ↦ s.1.trans' (s.1.trans' (s.2 h₁) h) (s.1.symm' (s.2 h₂))),
     ⟨Quotient.ind s.1.2.1, @fun x y ↦ Quotient.inductionOn₂ x y fun _ _ ↦ s.1.2.2,
       @fun x y z ↦ Quotient.inductionOn₃ x y z fun _ _ _ ↦ s.1.2.3⟩⟩
-  invFun s := ⟨comap Quotient.mk' s, fun x y h => by rw [comap_rel, eq_rel.2 h]⟩
+  invFun s := ⟨comap Quotient.mk' s, fun x y h => by rw [comap_rel, Quotient.eq'.2 h]⟩
   left_inv _ := rfl
   right_inv _ := ext fun x y ↦ Quotient.inductionOn₂ x y fun _ _ ↦ Iff.rfl
   map_rel_iff' :=
@@ -478,7 +485,6 @@ theorem Quotient.subsingleton_iff {s : Setoid α} : Subsingleton (Quotient s) 
   refine (surjective_quotient_mk' _).forall.trans (forall_congr' fun a => ?_)
   refine (surjective_quotient_mk' _).forall.trans (forall_congr' fun b => ?_)
   simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']
-  rfl
 
 theorem Quot.subsingleton_iff (r : α → α → Prop) :
     Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤ := by
diff --git a/Mathlib/Data/Setoid/Partition.lean b/Mathlib/Data/Setoid/Partition.lean
index b44853cfa153b..27e668bcb2ece 100644
--- a/Mathlib/Data/Setoid/Partition.lean
+++ b/Mathlib/Data/Setoid/Partition.lean
@@ -53,9 +53,9 @@ def mkClasses (c : Set (Set α)) (H : ∀ a, ∃! b ∈ c, a ∈ b) : Setoid α
 
 /-- Makes the equivalence classes of an equivalence relation. -/
 def classes (r : Setoid α) : Set (Set α) :=
-  { s | ∃ y, s = { x | r.Rel x y } }
+  { s | ∃ y, s = { x | r x y } }
 
-theorem mem_classes (r : Setoid α) (y) : { x | r.Rel x y } ∈ r.classes :=
+theorem mem_classes (r : Setoid α) (y) : { x | r x y } ∈ r.classes :=
   ⟨y, rfl⟩
 
 theorem classes_ker_subset_fiber_set {β : Type*} (f : α → β) :
@@ -74,17 +74,17 @@ theorem card_classes_ker_le {α β : Type*} [Fintype β] (f : α → β)
 
 /-- Two equivalence relations are equal iff all their equivalence classes are equal. -/
 theorem eq_iff_classes_eq {r₁ r₂ : Setoid α} :
-    r₁ = r₂ ↔ ∀ x, { y | r₁.Rel x y } = { y | r₂.Rel x y } :=
-  ⟨fun h _x => h ▸ rfl, fun h => ext' fun x => Set.ext_iff.1 <| h x⟩
+    r₁ = r₂ ↔ ∀ x, { y | r₁ x y } = { y | r₂ x y } :=
+  ⟨fun h _x => h ▸ rfl, fun h => ext fun x => Set.ext_iff.1 <| h x⟩
 
-theorem rel_iff_exists_classes (r : Setoid α) {x y} : r.Rel x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c :=
+theorem rel_iff_exists_classes (r : Setoid α) {x y} : r x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c :=
   ⟨fun h => ⟨_, r.mem_classes y, h, r.refl' y⟩, fun ⟨c, ⟨z, hz⟩, hx, hy⟩ => by
     subst c
     exact r.trans' hx (r.symm' hy)⟩
 
 /-- Two equivalence relations are equal iff their equivalence classes are equal. -/
 theorem classes_inj {r₁ r₂ : Setoid α} : r₁ = r₂ ↔ r₁.classes = r₂.classes :=
-  ⟨fun h => h ▸ rfl, fun h => ext' fun a b => by simp only [rel_iff_exists_classes, exists_prop, h]⟩
+  ⟨fun h => h ▸ rfl, fun h => ext fun a b => by simp only [rel_iff_exists_classes, exists_prop, h]⟩
 
 /-- The empty set is not an equivalence class. -/
 theorem empty_not_mem_classes {r : Setoid α} : ∅ ∉ r.classes := fun ⟨y, hy⟩ =>
@@ -92,7 +92,7 @@ theorem empty_not_mem_classes {r : Setoid α} : ∅ ∉ r.classes := fun ⟨y, h
 
 /-- Equivalence classes partition the type. -/
 theorem classes_eqv_classes {r : Setoid α} (a) : ∃! b ∈ r.classes, a ∈ b :=
-  ExistsUnique.intro { x | r.Rel x a } ⟨r.mem_classes a, r.refl' _⟩ <| by
+  ExistsUnique.intro { x | r x a } ⟨r.mem_classes a, r.refl' _⟩ <| by
     rintro y ⟨⟨_, rfl⟩, ha⟩
     ext x
     exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩
@@ -105,7 +105,7 @@ theorem eq_of_mem_classes {r : Setoid α} {x b} (hc : b ∈ r.classes) (hb : x 
 /-- The elements of a set of sets partitioning α are the equivalence classes of the
     equivalence relation defined by the set of sets. -/
 theorem eq_eqv_class_of_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {s y}
-    (hs : s ∈ c) (hy : y ∈ s) : s = { x | (mkClasses c H).Rel x y } := by
+    (hs : s ∈ c) (hy : y ∈ s) : s = { x | mkClasses c H x y } := by
   ext x
   constructor
   · intro hx _s' hs' hx'
@@ -117,11 +117,11 @@ theorem eq_eqv_class_of_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b
 /-- The equivalence classes of the equivalence relation defined by a set of sets
     partitioning α are elements of the set of sets. -/
 theorem eqv_class_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {y} :
-    { x | (mkClasses c H).Rel x y } ∈ c :=
+    { x | mkClasses c H x y } ∈ c :=
   (H y).elim fun _ hc _ => eq_eqv_class_of_mem H hc.1 hc.2 ▸ hc.1
 
 theorem eqv_class_mem' {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {x} :
-    { y : α | (mkClasses c H).Rel x y } ∈ c := by
+    { y : α | mkClasses c H x y } ∈ c := by
   convert @Setoid.eqv_class_mem _ _ H x using 3
   rw [Setoid.comm']
 
@@ -145,13 +145,13 @@ def setoidOfDisjointUnion {c : Set (Set α)} (hu : Set.sUnion c = @Set.univ α)
 /-- The equivalence relation made from the equivalence classes of an equivalence
     relation r equals r. -/
 theorem mkClasses_classes (r : Setoid α) : mkClasses r.classes classes_eqv_classes = r :=
-  ext' fun x _y =>
-    ⟨fun h => r.symm' (h { z | r.Rel z x } (r.mem_classes x) <| r.refl' x), fun h _b hb hx =>
+  ext fun x _y =>
+    ⟨fun h => r.symm' (h { z | r z x } (r.mem_classes x) <| r.refl' x), fun h _b hb hx =>
       eq_of_mem_classes (r.mem_classes x) (r.refl' x) hb hx ▸ r.symm' h⟩
 
 @[simp]
 theorem sUnion_classes (r : Setoid α) : ⋃₀ r.classes = Set.univ :=
-  Set.eq_univ_of_forall fun x => Set.mem_sUnion.2 ⟨{ y | r.Rel y x }, ⟨x, rfl⟩, Setoid.refl _⟩
+  Set.eq_univ_of_forall fun x => Set.mem_sUnion.2 ⟨{ y | r y x }, ⟨x, rfl⟩, Setoid.refl _⟩
 
 /-- The equivalence between the quotient by an equivalence relation and its
 type of equivalence classes. -/
@@ -177,8 +177,8 @@ noncomputable def quotientEquivClasses (r : Setoid α) : Quotient r ≃ Setoid.c
 
 @[simp]
 lemma quotientEquivClasses_mk_eq (r : Setoid α) (a : α) :
-    (quotientEquivClasses r (Quotient.mk r a) : Set α) = { x | r.Rel x a } :=
-  (@Subtype.ext_iff_val _ _ _ ⟨{ x | r.Rel x a }, Setoid.mem_classes r a⟩).mp rfl
+    (quotientEquivClasses r (Quotient.mk r a) : Set α) = { x | r x a } :=
+  (@Subtype.ext_iff_val _ _ _ ⟨{ x | r x a }, Setoid.mem_classes r a⟩).mp rfl
 
 section Partition
 
@@ -217,7 +217,7 @@ theorem IsPartition.sUnion_eq_univ {c : Set (Set α)} (hc : IsPartition c) : ⋃
 
 /-- All elements of a partition of α are the equivalence class of some y ∈ α. -/
 theorem exists_of_mem_partition {c : Set (Set α)} (hc : IsPartition c) {s} (hs : s ∈ c) :
-    ∃ y, s = { x | (mkClasses c hc.2).Rel x y } :=
+    ∃ y, s = { x | mkClasses c hc.2 x y } :=
   let ⟨y, hy⟩ := nonempty_of_mem_partition hc hs
   ⟨y, eq_eqv_class_of_mem hc.2 hs hy⟩
 
@@ -367,7 +367,7 @@ protected abbrev setoid (hs : IndexedPartition s) : Setoid α :=
 theorem index_some (i : ι) : hs.index (hs.some i) = i :=
   (mem_iff_index_eq _).1 <| hs.some_mem i
 
-theorem some_index (x : α) : hs.setoid.Rel (hs.some (hs.index x)) x :=
+theorem some_index (x : α) : hs.setoid (hs.some (hs.index x)) x :=
   hs.index_some (hs.index x)
 
 /-- The quotient associated to an indexed partition. -/
@@ -382,7 +382,7 @@ instance [Inhabited α] : Inhabited hs.Quotient :=
   ⟨hs.proj default⟩
 
 theorem proj_eq_iff {x y : α} : hs.proj x = hs.proj y ↔ hs.index x = hs.index y :=
-  Quotient.eq_rel
+  Quotient.eq''
 
 @[simp]
 theorem proj_some_index (x : α) : hs.proj (hs.some (hs.index x)) = hs.proj x :=
@@ -423,7 +423,7 @@ theorem index_out' (x : hs.Quotient) : hs.index x.out' = hs.index (hs.out x) :=
 theorem proj_out (x : hs.Quotient) : hs.proj (hs.out x) = x :=
   Quotient.inductionOn' x fun x => Quotient.sound' <| hs.some_index x
 
-theorem class_of {x : α} : setOf (hs.setoid.Rel x) = s (hs.index x) :=
+theorem class_of {x : α} : setOf (hs.setoid x) = s (hs.index x) :=
   Set.ext fun _y => eq_comm.trans hs.mem_iff_index_eq.symm
 
 theorem proj_fiber (x : hs.Quotient) : hs.proj ⁻¹' {x} = s (hs.equivQuotient.symm x) :=
diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
index 745facc0985ce..65ee8350a4451 100644
--- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
+++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
@@ -607,7 +607,7 @@ theorem tendsto_translationNumber_of_dist_bounded_aux (x : ℕ → ℝ) (C : ℝ
 theorem translationNumber_eq_of_dist_bounded {f g : CircleDeg1Lift} (C : ℝ)
     (H : ∀ n : ℕ, dist ((f ^ n) 0) ((g ^ n) 0) ≤ C) : τ f = τ g :=
   Eq.symm <| g.translationNumber_eq_of_tendsto_aux <|
-    f.tendsto_translationNumber_of_dist_bounded_aux _ C H
+    f.tendsto_translationNumber_of_dist_bounded_aux (fun n ↦ (g ^ n) 0) C H
 
 @[simp]
 theorem translationNumber_one : τ 1 = 0 :=
diff --git a/Mathlib/GroupTheory/Congruence/Defs.lean b/Mathlib/GroupTheory/Congruence/Defs.lean
index ced9c0f1660d1..118baa87520bd 100644
--- a/Mathlib/GroupTheory/Congruence/Defs.lean
+++ b/Mathlib/GroupTheory/Congruence/Defs.lean
@@ -166,7 +166,7 @@ theorem ext {c d : Con M} (H : ∀ x y, c x y ↔ d x y) : c = d :=
 @[to_additive "The map sending an additive congruence relation to its underlying equivalence
 relation is injective."]
 theorem toSetoid_inj {c d : Con M} (H : c.toSetoid = d.toSetoid) : c = d :=
-  ext <| ext_iff.1 H
+  ext <| Setoid.ext_iff.1 H
 
 /-- Two congruence relations are equal iff their underlying binary relations are equal. -/
 @[to_additive "Two additive congruence relations are equal iff their underlying binary relations
@@ -334,7 +334,7 @@ instance : InfSet (Con M) where
 @[to_additive "The infimum of a set of additive congruence relations is the same as the infimum of
 the set's image under the map to the underlying equivalence relation."]
 theorem sInf_toSetoid (S : Set (Con M)) : (sInf S).toSetoid = sInf (toSetoid '' S) :=
-  Setoid.ext' fun x y =>
+  Setoid.ext fun x y =>
     ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩
 
 /-- The infimum of a set of congruence relations is the same as the infimum of the set's image
@@ -572,8 +572,8 @@ def correspondence : { d // c ≤ d } ≃o Con c.Quotient where
     constructor
     · intros h x y hs
       rcases h ⟨x, y, rfl, rfl, hs⟩ with ⟨a, b, hx, hy, ht⟩
-      exact t.1.trans (t.1.symm <| t.2 <| Quotient.eq_rel.1 hx)
-        (t.1.trans ht (t.2 <| Quotient.eq_rel.1 hy))
+      exact t.1.trans (t.1.symm <| t.2 <| Quotient.eq'.1 hx)
+        (t.1.trans ht (t.2 <| Quotient.eq'.1 hy))
     · intros h _ _ hs
       rcases hs with ⟨a, b, hx, hy, Hs⟩
       exact ⟨a, b, hx, hy, h Hs⟩
diff --git a/Mathlib/GroupTheory/DoubleCoset.lean b/Mathlib/GroupTheory/DoubleCoset.lean
index a7d7e29638510..d80688cff9e27 100644
--- a/Mathlib/GroupTheory/DoubleCoset.lean
+++ b/Mathlib/GroupTheory/DoubleCoset.lean
@@ -72,15 +72,15 @@ def Quotient (H K : Set G) : Type _ :=
   _root_.Quotient (setoid H K)
 
 theorem rel_iff {H K : Subgroup G} {x y : G} :
-    (setoid ↑H ↑K).Rel x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b :=
+    setoid ↑H ↑K x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b :=
   Iff.trans
     ⟨fun (hxy : doset x H K = doset y H K) => hxy ▸ mem_doset_self H K y,
       fun hxy => (doset_eq_of_mem hxy).symm⟩ mem_doset
 
 theorem bot_rel_eq_leftRel (H : Subgroup G) :
-    (setoid ↑(⊥ : Subgroup G) ↑H).Rel = (QuotientGroup.leftRel H).Rel := by
+    ⇑(setoid ↑(⊥ : Subgroup G) ↑H) = ⇑(QuotientGroup.leftRel H) := by
   ext a b
-  rw [rel_iff, Setoid.Rel, QuotientGroup.leftRel_apply]
+  rw [rel_iff, QuotientGroup.leftRel_apply]
   constructor
   · rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
     change a⁻¹ * (1 * a * b) ∈ H
@@ -89,9 +89,9 @@ theorem bot_rel_eq_leftRel (H : Subgroup G) :
     exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩
 
 theorem rel_bot_eq_right_group_rel (H : Subgroup G) :
-    (setoid ↑H ↑(⊥ : Subgroup G)).Rel = (QuotientGroup.rightRel H).Rel := by
+    ⇑(setoid ↑H ↑(⊥ : Subgroup G)) = ⇑(QuotientGroup.rightRel H) := by
   ext a b
-  rw [rel_iff, Setoid.Rel, QuotientGroup.rightRel_apply]
+  rw [rel_iff, QuotientGroup.rightRel_apply]
   constructor
   · rintro ⟨b, hb, a, rfl : a = 1, rfl⟩
     change b * a * 1 * a⁻¹ ∈ H
diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean
index 9f99144a7769a..547d1fc8f93c9 100644
--- a/Mathlib/GroupTheory/GroupAction/Basic.lean
+++ b/Mathlib/GroupTheory/GroupAction/Basic.lean
@@ -373,12 +373,11 @@ def orbitRel : Setoid α where
 variable {G α}
 
 @[to_additive]
-theorem orbitRel_apply {a b : α} : (orbitRel G α).Rel a b ↔ a ∈ orbit G b :=
+theorem orbitRel_apply {a b : α} : orbitRel G α a b ↔ a ∈ orbit G b :=
   Iff.rfl
 
-@[to_additive]
-lemma orbitRel_r_apply {a b : α} : (orbitRel G _).r a b ↔ a ∈ orbit G b :=
-  Iff.rfl
+@[to_additive (attr := deprecated (since := "2024-10-18"))]
+alias orbitRel_r_apply := orbitRel_apply
 
 @[to_additive]
 lemma orbitRel_subgroup_le (H : Subgroup G) : orbitRel H α ≤ orbitRel G α :=
@@ -468,7 +467,7 @@ theorem pretransitive_iff_subsingleton_quotient :
   · refine Quot.inductionOn a (fun x ↦ ?_)
     exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)
   · have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
-    exact Quotient.eq_rel.mp h
+    exact Quotient.eq''.mp h
 
 /-- If `α` is non-empty, an action is pretransitive if and only if the quotient has exactly one
 element. -/
@@ -511,7 +510,7 @@ lemma orbitRel.Quotient.orbit_injective :
     Injective (orbitRel.Quotient.orbit : orbitRel.Quotient G α → Set α) := by
   intro x y h
   simp_rw [orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq', orbit_eq_iff,
-    ← orbitRel_r_apply] at h
+    ← orbitRel_apply] at h
   simpa [← Quotient.eq''] using h
 
 @[to_additive (attr := simp)]
@@ -596,7 +595,7 @@ lemma orbitRel.Quotient.mem_subgroup_orbit_iff' {H : Subgroup G} {x : orbitRel.Q
        at hb
     rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
     convert hb using 1
-    rw [orbit_eq_iff, ← orbitRel_r_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
+    rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
   rw [orbitRel.Quotient.mem_orbit, h, @Quotient.mk''_eq_mk]
 
 variable (G) (α)
@@ -725,7 +724,7 @@ theorem stabilizer_smul_eq_stabilizer_map_conj (g : G) (a : α) :
     inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
 
 /-- A bijection between the stabilizers of two elements in the same orbit. -/
-noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : (orbitRel G α).Rel a b) :
+noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : orbitRel G α a b) :
     stabilizer G a ≃* stabilizer G b :=
   let g : G := Classical.choose h
   have hg : g • b = a := Classical.choose_spec h
@@ -749,7 +748,7 @@ theorem stabilizer_vadd_eq_stabilizer_map_conj (g : G) (a : α) :
     AddAut.conj_symm_apply]
 
 /-- A bijection between the stabilizers of two elements in the same orbit. -/
-noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : (orbitRel G α).Rel a b) :
+noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : orbitRel G α a b) :
     stabilizer G a ≃+ stabilizer G b :=
   let g : G := Classical.choose h
   have hg : g +ᵥ b = a := Classical.choose_spec h
diff --git a/Mathlib/GroupTheory/GroupAction/ConjAct.lean b/Mathlib/GroupTheory/GroupAction/ConjAct.lean
index 1f5c561c568ef..866e1f3b36304 100644
--- a/Mathlib/GroupTheory/GroupAction/ConjAct.lean
+++ b/Mathlib/GroupTheory/GroupAction/ConjAct.lean
@@ -246,7 +246,7 @@ theorem fixedPoints_eq_center : fixedPoints (ConjAct G) G = center G := by
 theorem mem_orbit_conjAct {g h : G} : g ∈ orbit (ConjAct G) h ↔ IsConj g h := by
   rw [isConj_comm, isConj_iff, mem_orbit_iff]; rfl
 
-theorem orbitRel_conjAct : (orbitRel (ConjAct G) G).Rel = IsConj :=
+theorem orbitRel_conjAct : ⇑(orbitRel (ConjAct G) G) = IsConj :=
   funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct]
 
 theorem orbit_eq_carrier_conjClasses (g : G) :
diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean
index 3babc32ec4071..f58416df124ac 100644
--- a/Mathlib/GroupTheory/GroupAction/Quotient.lean
+++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean
@@ -329,8 +329,7 @@ noncomputable def equivSubgroupOrbitsSetoidComap (H : Subgroup α) (ω : Ω) :
     have hx := x.property
     simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
     rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk]⟩⟧) fun a b h ↦ by
-      change Setoid.Rel _ _ _ at h
-      rw [Setoid.comap_rel, Setoid.Rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
+      rw [Setoid.comap_rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
       simp only [orbitRel.Quotient.subgroup_quotient_eq_iff]
       exact h
   left_inv := by
@@ -373,7 +372,7 @@ noncomputable def equivSubgroupOrbitsQuotientGroup [IsPretransitive α β]
     orbitRel.Quotient H β ≃ α ⧸ H where
   toFun := fun q ↦ q.liftOn' (fun y ↦ (exists_smul_eq α y x).choose) (by
     intro y₁ y₂ h
-    rw [orbitRel_r_apply] at h
+    rw [orbitRel_apply] at h
     rw [Quotient.eq'', leftRel_eq]
     dsimp only
     rcases h with ⟨g, rfl⟩
@@ -389,12 +388,12 @@ noncomputable def equivSubgroupOrbitsQuotientGroup [IsPretransitive α β]
     intro g₁ g₂ h
     rw [leftRel_eq] at h
     simp only
-    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_r_apply]
+    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
     exact ⟨⟨_, h⟩, by simp [mul_smul]⟩)
   left_inv := fun y ↦ by
     induction' y using Quotient.inductionOn' with y
     simp only [Quotient.liftOn'_mk'']
-    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_r_apply]
+    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
     convert mem_orbit_self _
     rw [inv_smul_eq_iff, (exists_smul_eq α y x).choose_spec]
   right_inv := fun g ↦ by
diff --git a/Mathlib/GroupTheory/Subgroup/Saturated.lean b/Mathlib/GroupTheory/Subgroup/Saturated.lean
index 1d7d366b914ad..6cbc7b2c45d71 100644
--- a/Mathlib/GroupTheory/Subgroup/Saturated.lean
+++ b/Mathlib/GroupTheory/Subgroup/Saturated.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.Subgroup.Basic
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
 # Saturated subgroups
diff --git a/Mathlib/LinearAlgebra/BilinearMap.lean b/Mathlib/LinearAlgebra/BilinearMap.lean
index 0430d8a20645b..c720aff5ff9b6 100644
--- a/Mathlib/LinearAlgebra/BilinearMap.lean
+++ b/Mathlib/LinearAlgebra/BilinearMap.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro
 -/
 import Mathlib.Algebra.Module.Submodule.Ker
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 
 /-!
 # Basics on bilinear maps
diff --git a/Mathlib/LinearAlgebra/LinearPMap.lean b/Mathlib/LinearAlgebra/LinearPMap.lean
index ff0ddc27cc274..6cc05feeabb39 100644
--- a/Mathlib/LinearAlgebra/LinearPMap.lean
+++ b/Mathlib/LinearAlgebra/LinearPMap.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Moritz Doll
 -/
 import Mathlib.LinearAlgebra.Prod
-import Mathlib.Algebra.Module.Basic
 
 /-!
 # Partially defined linear maps
diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
index 8db7f46936b45..ea1242276149d 100644
--- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean
+++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Algebra.Algebra.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Pi
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Sort
diff --git a/Mathlib/LinearAlgebra/Span.lean b/Mathlib/LinearAlgebra/Span.lean
index 8e873cfc1c533..478735c139125 100644
--- a/Mathlib/LinearAlgebra/Span.lean
+++ b/Mathlib/LinearAlgebra/Span.lean
@@ -8,6 +8,7 @@ import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.Module.Submodule.EqLocus
 import Mathlib.Algebra.Module.Submodule.Equiv
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Ring.Idempotents
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Order.CompactlyGenerated.Basic
diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean
index 3e36cb114970b..e058bb5e8e9af 100644
--- a/Mathlib/MeasureTheory/Group/Measure.lean
+++ b/Mathlib/MeasureTheory/Group/Measure.lean
@@ -775,7 +775,7 @@ nonrec theorem _root_.MulEquiv.isHaarMeasure_map [BorelSpace G] [TopologicalGrou
     [TopologicalGroup H] (e : G ≃* H) (he : Continuous e) (hesymm : Continuous e.symm) :
     IsHaarMeasure (Measure.map e μ) :=
   let f : G ≃ₜ H := .mk e
-  isHaarMeasure_map μ e he e.surjective f.closedEmbedding.tendsto_cocompact
+  isHaarMeasure_map μ (e : G →* H) he e.surjective f.closedEmbedding.tendsto_cocompact
 
 /-- A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map`. -/
 instance _root_.ContinuousLinearEquiv.isAddHaarMeasure_map
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index 7a7ab5f8c32c6..3c03fb33601d8 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1975,6 +1975,13 @@ theorem quasiMeasurePreserving_symm (μ : Measure α) (e : α ≃ᵐ β) :
 
 end MeasurableEquiv
 
+namespace MeasureTheory.Measure
+variable {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+
+lemma comap_swap (μ : Measure (α × β)) : μ.comap Prod.swap = μ.map Prod.swap :=
+  (MeasurableEquiv.prodComm ..).comap_symm
+
+end MeasureTheory.Measure
 end
 
 set_option linter.style.longFile 2000
diff --git a/Mathlib/Order/Defs.lean b/Mathlib/Order/Defs.lean
index 7a46f0ce76cf7..75d603ee2c080 100644
--- a/Mathlib/Order/Defs.lean
+++ b/Mathlib/Order/Defs.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Batteries.Classes.Order
+import Batteries.Tactic.Trans
 import Mathlib.Data.Ordering.Basic
 import Mathlib.Tactic.Lemma
-import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.TypeStar
 
diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
index 84c4397e07ac6..8b546db30b150 100644
--- a/Mathlib/Order/Filter/Basic.lean
+++ b/Mathlib/Order/Filter/Basic.lean
@@ -83,6 +83,9 @@ instance inhabitedMem : Inhabited { s : Set α // s ∈ f } :=
 theorem filter_eq_iff : f = g ↔ f.sets = g.sets :=
   ⟨congr_arg _, filter_eq⟩
 
+@[simp] theorem sets_subset_sets : f.sets ⊆ g.sets ↔ g ≤ f := .rfl
+@[simp] theorem sets_ssubset_sets : f.sets ⊂ g.sets ↔ g < f := .rfl
+
 /-- An extensionality lemma that is useful for filters with good lemmas about `sᶜ ∈ f` (e.g.,
 `Filter.comap`, `Filter.coprod`, `Filter.Coprod`, `Filter.cofinite`). -/
 protected theorem coext (h : ∀ s, sᶜ ∈ f ↔ sᶜ ∈ g) : f = g :=
@@ -253,21 +256,20 @@ theorem mem_inf_iff_superset {f g : Filter α} {s : Set α} :
 
 section CompleteLattice
 
-/- We lift the complete lattice along the Galois connection `generate` / `sets`. Unfortunately,
-  we want to have different definitional equalities for some lattice operations. So we define them
-  upfront and change the lattice operations for the complete lattice instance. -/
-instance instCompleteLatticeFilter : CompleteLattice (Filter α) :=
-  { @OrderDual.instCompleteLattice _ (giGenerate α).liftCompleteLattice with
-    le := (· ≤ ·)
-    top := ⊤
-    le_top := fun _ _s hs => (mem_top.1 hs).symm ▸ univ_mem
-    inf := (· ⊓ ·)
-    inf_le_left := fun _ _ _ => mem_inf_of_left
-    inf_le_right := fun _ _ _ => mem_inf_of_right
-    le_inf := fun _ _ _ h₁ h₂ _s ⟨_a, ha, _b, hb, hs⟩ => hs.symm ▸ inter_mem (h₁ ha) (h₂ hb)
-    sSup := join ∘ 𝓟
-    le_sSup := fun _ _f hf _s hs => hs hf
-    sSup_le := fun _ _f hf _s hs _g hg => hf _ hg hs }
+/- Complete lattice structure on `Filter α`. -/
+instance instCompleteLatticeFilter : CompleteLattice (Filter α) where
+  le_sup_left _ _ _ h := h.1
+  le_sup_right _ _ _ h := h.2
+  sup_le _ _ _ h₁ h₂ _ h := ⟨h₁ h, h₂ h⟩
+  inf_le_left _ _ _ := mem_inf_of_left
+  inf_le_right _ _ _ := mem_inf_of_right
+  le_inf := fun _ _ _ h₁ h₂ _s ⟨_a, ha, _b, hb, hs⟩ => hs.symm ▸ inter_mem (h₁ ha) (h₂ hb)
+  le_sSup _ _ h₁ _ h₂ := h₂ h₁
+  sSup_le _ _ h₁ _ h₂ _ h₃ := h₁ _ h₃ h₂
+  sInf_le _ _ h₁ _ h₂ := by rw [← Filter.sSup_lowerBounds]; exact fun _ h₃ ↦ h₃ h₁ h₂
+  le_sInf _ _ h₁ _ h₂ := by rw [← Filter.sSup_lowerBounds] at h₂; exact h₂ h₁
+  le_top _ _ := univ_mem'
+  bot_le _ _ _ := trivial
 
 instance : Inhabited (Filter α) := ⟨⊥⟩
 
@@ -324,10 +326,6 @@ theorem mem_sup {f g : Filter α} {s : Set α} : s ∈ f ⊔ g ↔ s ∈ f ∧ s
 theorem union_mem_sup {f g : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s ∪ t ∈ f ⊔ g :=
   ⟨mem_of_superset hs subset_union_left, mem_of_superset ht subset_union_right⟩
 
-@[simp]
-theorem mem_sSup {x : Set α} {s : Set (Filter α)} : x ∈ sSup s ↔ ∀ f ∈ s, x ∈ (f : Filter α) :=
-  Iff.rfl
-
 @[simp]
 theorem mem_iSup {x : Set α} {f : ι → Filter α} : x ∈ iSup f ↔ ∀ i, x ∈ f i := by
   simp only [← Filter.mem_sets, iSup_sets_eq, mem_iInter]
@@ -337,7 +335,7 @@ theorem iSup_neBot {f : ι → Filter α} : (⨆ i, f i).NeBot ↔ ∃ i, (f i).
   simp [neBot_iff]
 
 theorem iInf_eq_generate (s : ι → Filter α) : iInf s = generate (⋃ i, (s i).sets) :=
-  show generate _ = generate _ from congr_arg _ <| congr_arg sSup <| (range_comp _ _).symm
+  eq_of_forall_le_iff fun _ ↦ by simp [le_generate_iff]
 
 theorem mem_iInf_of_mem {f : ι → Filter α} (i : ι) {s} (hs : s ∈ f i) : s ∈ ⨅ i, f i :=
   iInf_le f i hs
@@ -598,7 +596,7 @@ abbrev coframeMinimalAxioms : Coframe.MinimalAxioms (Filter α) :=
     iInf_sup_le_sup_sInf := fun f s t ⟨h₁, h₂⟩ => by
       classical
       rw [iInf_subtype']
-      rw [sInf_eq_iInf', iInf_sets_eq_finite, mem_iUnion] at h₂
+      rw [sInf_eq_iInf', ← Filter.mem_sets, iInf_sets_eq_finite, mem_iUnion] at h₂
       obtain ⟨u, hu⟩ := h₂
       rw [← Finset.inf_eq_iInf] at hu
       suffices ⨅ i : s, f ⊔ ↑i ≤ f ⊔ u.inf fun i => ↑i from this ⟨h₁, hu⟩
@@ -1572,10 +1570,6 @@ instance : LawfulFunctor (Filter : Type u → Type u) where
 theorem pure_sets (a : α) : (pure a : Filter α).sets = { s | a ∈ s } :=
   rfl
 
-@[simp]
-theorem mem_pure {a : α} {s : Set α} : s ∈ (pure a : Filter α) ↔ a ∈ s :=
-  Iff.rfl
-
 @[simp]
 theorem eventually_pure {a : α} {p : α → Prop} : (∀ᶠ x in pure a, p x) ↔ p a :=
   Iff.rfl
diff --git a/Mathlib/Order/Filter/Defs.lean b/Mathlib/Order/Filter/Defs.lean
index cd23371bb3f2f..06e6369f2f301 100644
--- a/Mathlib/Order/Filter/Defs.lean
+++ b/Mathlib/Order/Filter/Defs.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Jeremy Avigad
 -/
 import Mathlib.Data.Set.Basic
 import Mathlib.Order.SetNotation
+import Mathlib.Order.Bounds.Defs
 
 /-!
 # Definitions about filters
@@ -141,6 +142,15 @@ scoped notation "𝓟" => Filter.principal
 
 @[simp] theorem mem_principal : s ∈ 𝓟 t ↔ t ⊆ s := Iff.rfl
 
+/-- `pure x` is the set of sets that contain `x`. It is equal to `𝓟 {x}` but
+with this definition we have `s ∈ pure a` defeq `a ∈ s`. -/
+instance : Pure Filter where
+  pure x := .copy (𝓟 {x}) {s | x ∈ s} fun _ ↦ by simp
+
+@[simp]
+theorem mem_pure {a : α} {s : Set α} : s ∈ (pure a : Filter α) ↔ a ∈ s :=
+  Iff.rfl
+
 /-- The *kernel* of a filter is the intersection of all its sets. -/
 def ker (f : Filter α) : Set α := ⋂₀ f.sets
 
@@ -164,11 +174,25 @@ instance : PartialOrder (Filter α) where
 theorem le_def : f ≤ g ↔ ∀ x ∈ g, x ∈ f :=
   Iff.rfl
 
-instance : Top (Filter α) :=
-  ⟨{  sets := { s | ∀ x, x ∈ s }
-      univ_sets := fun x => mem_univ x
-      sets_of_superset := fun hx hxy a => hxy (hx a)
-      inter_sets := fun hx hy _ => mem_inter (hx _) (hy _) }⟩
+instance instSupSet : SupSet (Filter α) where
+  sSup S := join (𝓟 S)
+
+@[simp] theorem mem_sSup {S : Set (Filter α)} : s ∈ sSup S ↔ ∀ f ∈ S, s ∈ f := .rfl
+
+/-- Infimum of a set of filters.
+This definition is marked as irreducible
+so that Lean doesn't try to unfold it when unifying expressions. -/
+@[irreducible]
+protected def sInf (s : Set (Filter α)) : Filter α := sSup (lowerBounds s)
+
+instance instInfSet : InfSet (Filter α) where
+  sInf := Filter.sInf
+
+protected theorem sSup_lowerBounds (s : Set (Filter α)) : sSup (lowerBounds s) = sInf s := by
+  simp [sInf, Filter.sInf]
+
+instance : Top (Filter α) where
+  top := .copy (sSup (Set.range pure)) {s | ∀ x, x ∈ s} <| by simp
 
 theorem mem_top_iff_forall {s : Set α} : s ∈ (⊤ : Filter α) ↔ ∀ x, x ∈ s :=
   Iff.rfl
@@ -178,11 +202,7 @@ theorem mem_top {s : Set α} : s ∈ (⊤ : Filter α) ↔ s = univ := by
   rw [mem_top_iff_forall, eq_univ_iff_forall]
 
 instance : Bot (Filter α) where
-  bot :=
-    { sets := univ
-      univ_sets := trivial
-      sets_of_superset := fun _ _ ↦ trivial
-      inter_sets := fun _ _ ↦ trivial }
+  bot := .copy (sSup ∅) univ <| by simp
 
 @[simp]
 theorem mem_bot {s : Set α} : s ∈ (⊥ : Filter α) :=
@@ -190,7 +210,7 @@ theorem mem_bot {s : Set α} : s ∈ (⊥ : Filter α) :=
 
 /-- The infimum of filters is the filter generated by intersections
   of elements of the two filters. -/
-instance : Inf (Filter α) :=
+instance instInf : Inf (Filter α) :=
   ⟨fun f g : Filter α =>
     { sets := { s | ∃ a ∈ f, ∃ b ∈ g, s = a ∩ b }
       univ_sets := ⟨_, univ_mem, _, univ_mem, by simp⟩
@@ -205,12 +225,8 @@ instance : Inf (Filter α) :=
         ac_rfl }⟩
 
 /-- The supremum of two filters is the filter that contains sets that belong to both filters. -/
-instance : Sup (Filter α) where
-  sup f g :=
-    { sets := {s | s ∈ f ∧ s ∈ g}
-      univ_sets := ⟨univ_mem, univ_mem⟩
-      sets_of_superset := fun h₁ h₂ ↦ ⟨mem_of_superset h₁.1 h₂, mem_of_superset h₁.2 h₂⟩
-      inter_sets := fun h₁ h₂ ↦ ⟨inter_mem h₁.1 h₂.1, inter_mem h₁.2 h₂.2⟩ }
+instance instSup : Sup (Filter α) where
+  sup f g := .copy (sSup {f, g}) {s | s ∈ f ∧ s ∈ g} <| by simp
 
 /-- A filter is `NeBot` if it is not equal to `⊥`, or equivalently the empty set does not belong to
 the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a
@@ -319,15 +335,6 @@ in adding quantifiers to the middle of `Tendsto`s. See
 def curry (f : Filter α) (g : Filter β) : Filter (α × β) :=
   bind f fun a ↦ map (a, ·) g
 
-/-- `pure x` is the set of sets that contain `x`. It is equal to `𝓟 {x}` but
-with this definition we have `s ∈ pure a` defeq `a ∈ s`. -/
-instance : Pure Filter :=
-  ⟨fun x =>
-    { sets := { s | x ∈ s }
-      inter_sets := And.intro
-      sets_of_superset := fun hs hst => hst hs
-      univ_sets := trivial }⟩
-
 instance : Bind Filter :=
   ⟨@Filter.bind⟩
 
diff --git a/Mathlib/Order/InitialSeg.lean b/Mathlib/Order/InitialSeg.lean
index e53d78efa0277..b1e211077acf2 100644
--- a/Mathlib/Order/InitialSeg.lean
+++ b/Mathlib/Order/InitialSeg.lean
@@ -289,6 +289,10 @@ theorem mem_range_of_rel [IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s
 @[deprecated mem_range_of_rel (since := "2024-09-21")]
 alias init := mem_range_of_rel
 
+theorem surjOn (f : r ≺i s) : Set.SurjOn f Set.univ { b | s b f.top } := by
+  intro b h
+  simpa using mem_range_of_rel_top _ h
+
 /-- A principal segment is in particular an initial segment. -/
 instance hasCoeInitialSeg [IsTrans β s] : Coe (r ≺i s) (r ≼i s) :=
   ⟨fun f => ⟨f.toRelEmbedding, fun _ _ => f.mem_range_of_rel⟩⟩
@@ -383,6 +387,9 @@ instance [IsWellOrder β s] : Subsingleton (r ≺i s) :=
     cases g
     have := RelEmbedding.coe_fn_injective ef; congr ⟩
 
+protected theorem eq [IsWellOrder β s] (f g : r ≺i s) (a) : f a = g a := by
+  rw [Subsingleton.elim f g]
+
 theorem top_eq [IsWellOrder γ t] (e : r ≃r s) (f : r ≺i t) (g : s ≺i t) : f.top = g.top := by
   rw [Subsingleton.elim f (PrincipalSeg.equivLT e g)]; rfl
 
diff --git a/Mathlib/Order/Partition/Finpartition.lean b/Mathlib/Order/Partition/Finpartition.lean
index 2392533c815c4..0c1bbdebaec82 100644
--- a/Mathlib/Order/Partition/Finpartition.lean
+++ b/Mathlib/Order/Partition/Finpartition.lean
@@ -581,12 +581,12 @@ def ofSetoid (s : Setoid α) [DecidableRel s.r] : Finpartition (univ : Finset α
   sup_parts := by
     ext a
     simp only [sup_image, Function.id_comp, mem_univ, mem_sup, mem_filter, true_and, iff_true]
-    use a; exact s.refl a
+    use a
   not_bot_mem := by
     rw [bot_eq_empty, mem_image, not_exists]
     intro a
     simp only [filter_eq_empty_iff, not_forall, mem_univ, forall_true_left, true_and, not_not]
-    use a; exact s.refl a
+    use a
 
 theorem mem_part_ofSetoid_iff_rel {s : Setoid α} [DecidableRel s.r] {b : α} :
     b ∈ (ofSetoid s).part a ↔ s.r a b := by
diff --git a/Mathlib/RingTheory/AdicCompletion/Algebra.lean b/Mathlib/RingTheory/AdicCompletion/Algebra.lean
index f9ab3648fed20..6f7c6168e2c6c 100644
--- a/Mathlib/RingTheory/AdicCompletion/Algebra.lean
+++ b/Mathlib/RingTheory/AdicCompletion/Algebra.lean
@@ -197,7 +197,7 @@ theorem smul_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R)
 good definitional behaviour for the module instance on adic completions -/
 instance : SMul (R ⧸ (I • ⊤ : Ideal R)) (M ⧸ (I • ⊤ : Submodule R M)) where
   smul r x :=
-    Quotient.liftOn r (· • x) fun b₁ b₂ (h : Setoid.Rel _ b₁ b₂) ↦ by
+    Quotient.liftOn r (· • x) fun b₁ b₂ h ↦ by
       refine Quotient.inductionOn' x (fun x ↦ ?_)
       have h : b₁ - b₂ ∈ (I : Submodule R R) := by
         rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_def]
diff --git a/Mathlib/RingTheory/Congruence/Basic.lean b/Mathlib/RingTheory/Congruence/Basic.lean
index 131575077c37b..90eea0cd93488 100644
--- a/Mathlib/RingTheory/Congruence/Basic.lean
+++ b/Mathlib/RingTheory/Congruence/Basic.lean
@@ -74,7 +74,7 @@ instance : FunLike (RingCon R) R (R → Prop) where
     rcases x with ⟨⟨x, _⟩, _⟩
     rcases y with ⟨⟨y, _⟩, _⟩
     congr!
-    rw [Setoid.ext_iff, (show x.Rel = y.Rel from h)]
+    rw [Setoid.ext_iff, (show ⇑x = ⇑y from h)]
     simp
 
 theorem rel_eq_coe : c.r = c :=
@@ -445,7 +445,7 @@ instance : InfSet (RingCon R) where
 /-- The infimum of a set of congruence relations is the same as the infimum of the set's image
     under the map to the underlying equivalence relation. -/
 theorem sInf_toSetoid (S : Set (RingCon R)) : (sInf S).toSetoid = sInf ((·.toSetoid) '' S) :=
-  Setoid.ext' fun x y =>
+  Setoid.ext fun x y =>
     ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩
 
 /-- The infimum of a set of congruence relations is the same as the infimum of the set's image
diff --git a/Mathlib/RingTheory/Nilpotent/Basic.lean b/Mathlib/RingTheory/Nilpotent/Basic.lean
index 71e196c394db9..9eddb6417010a 100644
--- a/Mathlib/RingTheory/Nilpotent/Basic.lean
+++ b/Mathlib/RingTheory/Nilpotent/Basic.lean
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Associated.Basic
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Group.Action.Prod
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Data.Nat.Lattice
diff --git a/Mathlib/RingTheory/Valuation/ValuationRing.lean b/Mathlib/RingTheory/Valuation/ValuationRing.lean
index e95d7d322ff0d..266cd8e9d5884 100644
--- a/Mathlib/RingTheory/Valuation/ValuationRing.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationRing.lean
@@ -142,22 +142,22 @@ noncomputable instance linearOrder : LinearOrder (ValueGroup A K) where
 noncomputable instance linearOrderedCommGroupWithZero :
     LinearOrderedCommGroupWithZero (ValueGroup A K) :=
   { linearOrder .. with
-    mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]; apply Setoid.refl'
-    one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]; apply Setoid.refl'
-    mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]; apply Setoid.refl'
-    mul_comm := by rintro ⟨a⟩ ⟨b⟩; apply Quotient.sound'; rw [mul_comm]; apply Setoid.refl'
+    mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]
+    one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]
+    mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]
+    mul_comm := by rintro ⟨a⟩ ⟨b⟩; apply Quotient.sound'; rw [mul_comm]
     mul_le_mul_left := by
       rintro ⟨a⟩ ⟨b⟩ ⟨c, rfl⟩ ⟨d⟩
       use c; simp only [Algebra.smul_def]; ring
-    zero_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]; apply Setoid.refl'
-    mul_zero := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_zero]; apply Setoid.refl'
+    zero_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]
+    mul_zero := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_zero]
     zero_le_one := ⟨0, by rw [zero_smul]⟩
     exists_pair_ne := by
       use 0, 1
       intro c; obtain ⟨d, hd⟩ := Quotient.exact' c
       apply_fun fun t => d⁻¹ • t at hd
       simp only [inv_smul_smul, smul_zero, one_ne_zero] at hd
-    inv_zero := by apply Quotient.sound'; rw [inv_zero]; apply Setoid.refl'
+    inv_zero := by apply Quotient.sound'; rw [inv_zero]
     mul_inv_cancel := by
       rintro ⟨a⟩ ha
       apply Quotient.sound'
diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean
index 2de607c6ac406..bc2a81d9ed4ff 100644
--- a/Mathlib/SetTheory/Ordinal/Basic.lean
+++ b/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -139,11 +139,6 @@ instance inhabited : Inhabited Ordinal :=
 instance one : One Ordinal :=
   ⟨type <| @EmptyRelation PUnit⟩
 
-/-- The order type of an element inside a well order. For the embedding as a principal segment, see
-`typein.principalSeg`. -/
-def typein (r : α → α → Prop) [IsWellOrder α r] (a : α) : Ordinal :=
-  type (Subrel r { b | r b a })
-
 @[simp]
 theorem type_def' (w : WellOrder) : ⟦w⟧ = type w.r := by
   cases w
@@ -375,69 +370,73 @@ def principalSegToType {α β : Ordinal} (h : α < β) : α.toType <i β.toType
 @[deprecated principalSegToType (since := "2024-08-26")]
 noncomputable alias principalSegOut := principalSegToType
 
+/-- The order type of an element inside a well order.
+
+This is registered as a principal segment embedding into the ordinals, with top `type r`. -/
+def typein (r : α → α → Prop) [IsWellOrder α r] : @PrincipalSeg α Ordinal.{u} r (· < ·) := by
+  refine ⟨RelEmbedding.ofMonotone _ fun a b ha ↦
+    ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r, fun a ↦ ⟨?_, ?_⟩⟩
+  · rintro ⟨c, hc⟩
+    exact trans hc ha
+  · exact ha
+  · rintro ⟨b, rfl⟩
+    exact (PrincipalSeg.ofElement _ _).ordinal_type_lt
+  · refine inductionOn a ?_
+    rintro β s wo ⟨g⟩
+    exact ⟨_, g.subrelIso.ordinal_type_eq⟩
+
+@[deprecated typein (since := "2024-10-09")]
+alias typein.principalSeg := typein
+
+set_option linter.deprecated false in
+@[deprecated (since := "2024-10-09")]
+theorem typein.principalSeg_coe (r : α → α → Prop) [IsWellOrder α r] :
+    (typein.principalSeg r : α → Ordinal) = typein r :=
+  rfl
+
+@[simp]
+theorem type_subrel (r : α → α → Prop) [IsWellOrder α r] (a : α) :
+    type (Subrel r { b | r b a }) = typein r a :=
+  rfl
+
+@[simp]
+theorem top_typein (r : α → α → Prop) [IsWellOrder α r] : (typein r).top = type r :=
+  rfl
+
 theorem typein_lt_type (r : α → α → Prop) [IsWellOrder α r] (a : α) : typein r a < type r :=
-  ⟨PrincipalSeg.ofElement _ _⟩
+  (typein r).lt_top a
 
 theorem typein_lt_self {o : Ordinal} (i : o.toType) : typein (α := o.toType) (· < ·) i < o := by
   simp_rw [← type_lt o]
   apply typein_lt_type
 
 @[simp]
-theorem typein_top {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
-    (f : r ≺i s) : typein s f.top = type r :=
-  Eq.symm <|
-    Quot.sound
-      ⟨RelIso.ofSurjective (RelEmbedding.codRestrict _ f f.lt_top) fun ⟨a, h⟩ => by
-          rcases f.mem_range_of_rel_top h with ⟨b, rfl⟩; exact ⟨b, rfl⟩⟩
-
-@[simp]
-theorem typein_apply {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
-    (f : r ≼i s) (a : α) : Ordinal.typein s (f a) = Ordinal.typein r a :=
-  Eq.symm <|
-    Quotient.sound
-      ⟨RelIso.ofSurjective
-        (RelEmbedding.codRestrict _ ((Subrel.relEmbedding _ _).trans f) fun ⟨x, h⟩ => by
-          rw [RelEmbedding.trans_apply]; exact f.toRelEmbedding.map_rel_iff.2 h)
-          fun ⟨y, h⟩ => by
-            rcases f.mem_range_of_rel h with ⟨a, rfl⟩
-            exact ⟨⟨a, f.toRelEmbedding.map_rel_iff.1 h⟩,
-              Subtype.eq <| RelEmbedding.trans_apply _ _ _⟩⟩
+theorem typein_top {α β} {r : α → α → Prop} {s : β → β → Prop}
+    [IsWellOrder α r] [IsWellOrder β s] (f : r ≺i s) : typein s f.top = type r :=
+  f.subrelIso.ordinal_type_eq
 
 @[simp]
 theorem typein_lt_typein (r : α → α → Prop) [IsWellOrder α r] {a b : α} :
     typein r a < typein r b ↔ r a b :=
-  ⟨fun ⟨f⟩ => by
-    have : f.top.1 = a := by
-      let f' := PrincipalSeg.ofElement r a
-      let g' := f.trans (PrincipalSeg.ofElement r b)
-      have : g'.top = f'.top := by rw [Subsingleton.elim f' g']
-      exact this
-    rw [← this]
-    exact f.top.2, fun h =>
-    ⟨PrincipalSeg.codRestrict _ (PrincipalSeg.ofElement r a) (fun x => @trans _ r _ _ _ _ x.2 h) h⟩⟩
+  (typein r).map_rel_iff
+
+theorem mem_range_typein_iff (r : α → α → Prop) [IsWellOrder α r] {o} :
+    o ∈ Set.range (typein r) ↔ o < type r :=
+  (typein r).mem_range_iff_rel
 
 theorem typein_surj (r : α → α → Prop) [IsWellOrder α r] {o} (h : o < type r) :
-    ∃ a, typein r a = o :=
-  inductionOn o (fun _ _ _ ⟨f⟩ => ⟨f.top, typein_top _⟩) h
+    o ∈ Set.range (typein r) :=
+  (typein r).mem_range_of_rel_top h
+
+theorem typein_surjOn (r : α → α → Prop) [IsWellOrder α r] :
+    Set.SurjOn (typein r) Set.univ (Set.Iio (type r)) :=
+  (typein r).surjOn
 
 theorem typein_injective (r : α → α → Prop) [IsWellOrder α r] : Injective (typein r) :=
-  injective_of_increasing r (· < ·) (typein r) (typein_lt_typein r).2
+  (typein r).injective
 
-@[simp]
 theorem typein_inj (r : α → α → Prop) [IsWellOrder α r] {a b} : typein r a = typein r b ↔ a = b :=
-  (typein_injective r).eq_iff
-
-/-- Principal segment version of the `typein` function, embedding a well order into ordinals as a
-principal segment. -/
-def typein.principalSeg {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :
-    @PrincipalSeg α Ordinal.{u} r (· < ·) :=
-  ⟨⟨⟨typein r, typein_injective r⟩, typein_lt_typein r⟩, type r,
-    fun _ ↦ ⟨fun ⟨a, h⟩ ↦ h ▸ typein_lt_type r a, typein_surj r⟩⟩
-
-@[simp]
-theorem typein.principalSeg_coe (r : α → α → Prop) [IsWellOrder α r] :
-    (typein.principalSeg r : α → Ordinal) = typein r :=
-  rfl
+  (typein r).inj
 
 /-! ### Enumerating elements in a well-order with ordinals. -/
 
@@ -450,16 +449,16 @@ the elements of `α`. -/
 @[simps! symm_apply_coe]
 def enum (r : α → α → Prop) [IsWellOrder α r] :
     @RelIso { o // o < type r } α (Subrel (· < ·) { o | o < type r }) r :=
-  (typein.principalSeg r).subrelIso
+  (typein r).subrelIso
 
 @[simp]
 theorem typein_enum (r : α → α → Prop) [IsWellOrder α r] {o} (h : o < type r) :
     typein r (enum r ⟨o, h⟩) = o :=
-  (typein.principalSeg r).apply_subrelIso _
+  (typein r).apply_subrelIso _
 
 theorem enum_type {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
     (f : s ≺i r) {h : type s < type r} : enum r ⟨type s, h⟩ = f.top :=
-  (typein.principalSeg r).injective <| (typein_enum _ _).trans (typein_top _).symm
+  (typein r).injective <| (typein_enum _ _).trans (typein_top _).symm
 
 @[simp]
 theorem enum_typein (r : α → α → Prop) [IsWellOrder α r] (a : α) :
@@ -502,6 +501,10 @@ theorem induction {p : Ordinal.{u} → Prop} (i : Ordinal.{u}) (h : ∀ j, (∀
     p i :=
   lt_wf.induction i h
 
+theorem typein_apply {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
+    (f : r ≼i s) (a : α) : typein s (f a) = typein r a := by
+  rw [← f.leLT_apply _ a, (f.leLT _).eq]
+
 /-! ### Cardinality of ordinals -/
 
 
@@ -1031,7 +1034,7 @@ def liftPrincipalSeg : Ordinal.{u} <i Ordinal.{max (u + 1) v} :=
       rw [← e]
       refine inductionOn a ?_
       intro α r _
-      exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein.principalSeg r⟩
+      exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩
     · rw [← lift_id (type s)] at h ⊢
       cases' lift_type_lt.{_,_,v}.1 h with f
       cases' f with f a hf
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index cd494193a67b4..efac05b1b7da1 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -203,7 +203,6 @@ import Mathlib.Tactic.ReduceModChar
 import Mathlib.Tactic.ReduceModChar.Ext
 import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm
-import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
index f9c7a25eb782c..c864e4fc60f26 100644
--- a/Mathlib/Tactic/Common.lean
+++ b/Mathlib/Tactic/Common.lean
@@ -79,7 +79,6 @@ import Mathlib.Tactic.PushNeg
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recover
 import Mathlib.Tactic.Relation.Rfl
-import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Says
diff --git a/Mathlib/Tactic/MoveAdd.lean b/Mathlib/Tactic/MoveAdd.lean
index 094ce46b60265..87cf3bdb6add4 100644
--- a/Mathlib/Tactic/MoveAdd.lean
+++ b/Mathlib/Tactic/MoveAdd.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Damiano Testa
 -/
 import Mathlib.Algebra.Group.Basic
+import Mathlib.Lean.Meta
 
 /-!
 
diff --git a/Mathlib/Tactic/Relation/Trans.lean b/Mathlib/Tactic/Relation/Trans.lean
deleted file mode 100644
index 290d23e9aeb70..0000000000000
--- a/Mathlib/Tactic/Relation/Trans.lean
+++ /dev/null
@@ -1,222 +0,0 @@
-/-
-Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Siddhartha Gadgil, Mario Carneiro
--/
-import Mathlib.Lean.Meta
-import Mathlib.Lean.Elab.Tactic.Basic
-import Lean.Elab.Tactic.ElabTerm
-import Mathlib.Tactic.TypeStar
-
-/-!
-# `trans` tactic
-
-This implements the `trans` tactic, which can apply transitivity theorems with an optional middle
-variable argument.
--/
-
-namespace Mathlib.Tactic
-open Lean Meta Elab
-
-initialize registerTraceClass `Tactic.trans
-
-/-- Discrimation tree settings for the `trans` extension. -/
-def transExt.config : WhnfCoreConfig := {}
-
-/-- Environment extension storing transitivity lemmas -/
-initialize transExt :
-    SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
-  registerSimpleScopedEnvExtension {
-    addEntry := fun dt (n, ks) ↦ dt.insertCore ks n
-    initial := {}
-  }
-
-initialize registerBuiltinAttribute {
-  name := `trans
-  descr := "transitive relation"
-  add := fun decl _ kind ↦ MetaM.run' do
-    let declTy := (← getConstInfo decl).type
-    let (xs, _, targetTy) ← withReducible <| forallMetaTelescopeReducing declTy
-    let fail := throwError
-      "@[trans] attribute only applies to lemmas proving
-      x ∼ y → y ∼ z → x ∼ z, got {indentExpr declTy} with target {indentExpr targetTy}"
-    let .app (.app rel _) _ := targetTy | fail
-    let some yzHyp := xs.back? | fail
-    let some xyHyp := xs.pop.back? | fail
-    let .app (.app _ _) _ ← inferType yzHyp | fail
-    let .app (.app _ _) _ ← inferType xyHyp | fail
-    let key ← withReducible <| DiscrTree.mkPath rel transExt.config
-    transExt.add (decl, key) kind
-}
-
-universe u v in
-/-- Composition using the `Trans` class in the homogeneous case. -/
-def _root_.Trans.simple {α : Sort u} {r : α → α → Sort v} {a b c : α} [Trans r r r] :
-    r a b → r b c → r a c := trans
-
-universe u v w in
-/-- Composition using the `Trans` class in the general case. -/
-def _root_.Trans.het {α β γ : Sort*} {a : α} {b : β} {c : γ}
-    {r : α → β → Sort u} {s : β → γ → Sort v} {t : outParam (α → γ → Sort w)} [Trans r s t] :
-    r a b → s b c → t a c := trans
-
-open Lean.Elab.Tactic
-
-/-- solving `e ← mkAppM' f #[x]` -/
-def getExplicitFuncArg? (e : Expr) : MetaM (Option <| Expr × Expr) := do
-  match e with
-  | Expr.app f a => do
-    if ← isDefEq (← mkAppM' f #[a]) e then
-      return some (f, a)
-    else
-      getExplicitFuncArg? f
-  | _ => return none
-
-/-- solving `tgt ← mkAppM' rel #[x, z]` given `tgt = f z` -/
-def getExplicitRelArg? (tgt f z : Expr) : MetaM (Option <| Expr × Expr) := do
-  match f with
-  | Expr.app rel x => do
-    let check: Bool ← do
-      try
-        let folded ← mkAppM' rel #[x, z]
-        isDefEq folded tgt
-      catch _ =>
-        pure false
-    if check then
-      return some (rel, x)
-    else
-      getExplicitRelArg? tgt rel z
-  | _ => return none
-
-/-- refining `tgt ← mkAppM' rel #[x, z]` dropping more arguments if possible -/
-def getExplicitRelArgCore (tgt rel x z : Expr) : MetaM (Expr × Expr) := do
-  match rel with
-  | Expr.app rel' _ => do
-    let check: Bool ← do
-      try
-        let folded ← mkAppM' rel' #[x, z]
-        isDefEq folded tgt
-      catch _ =>
-        pure false
-    if !check then
-      return (rel, x)
-    else
-      getExplicitRelArgCore tgt rel' x z
-  | _ => return (rel ,x)
-
-/-- Internal definition for `trans` tactic. Either a binary relation or a non-dependent
-arrow. -/
-inductive TransRelation
-  | app (rel : Expr)
-  | implies (name : Name) (bi : BinderInfo)
-
-/-- Finds an explicit binary relation in the argument, if possible. -/
-def getRel (tgt : Expr) : MetaM (Option (TransRelation × Expr × Expr)) := do
-  match tgt with
-  | .forallE name binderType body info => return .some (.implies name info, binderType, body)
-  | .app f z =>
-    match (← getExplicitRelArg? tgt f z) with
-    | some (rel, x) =>
-      let (rel, x) ← getExplicitRelArgCore tgt rel x z
-      return some (.app rel, x, z)
-    | none =>
-      return none
-  | _ => return none
-
-/--
-`trans` applies to a goal whose target has the form `t ~ u` where `~` is a transitive relation,
-that is, a relation which has a transitivity lemma tagged with the attribute [trans].
-
-* `trans s` replaces the goal with the two subgoals `t ~ s` and `s ~ u`.
-* If `s` is omitted, then a metavariable is used instead.
-
-Additionally, `trans` also applies to a goal whose target has the form `t → u`,
-in which case it replaces the goal with `t → s` and `s → u`.
--/
-elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do
-  let tgt ← getMainTarget''
-  let .some (rel, x, z) ← getRel tgt |
-    throwError (m!"transitivity lemmas only apply to binary relations and " ++
-                m!"non-dependent arrows, not {indentExpr tgt}")
-  match rel with
-  | .implies name info =>
-    -- only consider non-dependent arrows
-    if z.hasLooseBVars then
-      throwError "`trans` is not implemented for dependent arrows{indentExpr tgt}"
-    -- parse the intermeditate term
-    let middleType ← mkFreshExprMVar none
-    let t'? ← t?.mapM (elabTermWithHoles · middleType (← getMainTag))
-    let middle ← (t'?.map (pure ·.1)).getD (mkFreshExprMVar middleType)
-    liftMetaTactic fun goal => do
-      -- create two new goals
-      let g₁ ← mkFreshExprMVar (some <| .forallE name x middle info) .synthetic
-      let g₂ ← mkFreshExprMVar (some <| .forallE name middle z info) .synthetic
-      -- close the original goal with `fun x => g₂ (g₁ x)`
-      goal.assign (.lam name x (.app g₂ (.app g₁ (.bvar 0))) .default)
-      pure <| [g₁.mvarId!, g₂.mvarId!] ++ if let some (_, gs') := t'? then gs' else [middle.mvarId!]
-    return
-  | .app rel =>
-    trace[Tactic.trans]"goal decomposed"
-    trace[Tactic.trans]"rel: {indentExpr rel}"
-    trace[Tactic.trans]"x: {indentExpr x}"
-    trace[Tactic.trans]"z: {indentExpr z}"
-    -- first trying the homogeneous case
-    try
-      let ty ← inferType x
-      let t'? ← t?.mapM (elabTermWithHoles · ty (← getMainTag))
-      let s ← saveState
-      trace[Tactic.trans]"trying homogeneous case"
-      let lemmas :=
-        (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push ``Trans.simple
-      for lem in lemmas do
-        trace[Tactic.trans]"trying lemma {lem}"
-        try
-          liftMetaTactic fun g ↦ do
-            let lemTy ← inferType (← mkConstWithLevelParams lem)
-            let arity ← withReducible <| forallTelescopeReducing lemTy fun es _ ↦ pure es.size
-            let y ← (t'?.map (pure ·.1)).getD (mkFreshExprMVar ty)
-            let g₁ ← mkFreshExprMVar (some <| ← mkAppM' rel #[x, y]) .synthetic
-            let g₂ ← mkFreshExprMVar (some <| ← mkAppM' rel #[y, z]) .synthetic
-            g.assign (← mkAppOptM lem (mkArray (arity - 2) none ++ #[some g₁, some g₂]))
-            pure <| [g₁.mvarId!, g₂.mvarId!] ++
-              if let some (_, gs') := t'? then gs' else [y.mvarId!]
-          return
-        catch _ => s.restore
-      pure ()
-    catch _ =>
-    trace[Tactic.trans]"trying heterogeneous case"
-    let t'? ← t?.mapM (elabTermWithHoles · none (← getMainTag))
-    let s ← saveState
-    for lem in (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push
-        ``HEq.trans |>.push ``HEq.trans do
-      try
-        liftMetaTactic fun g ↦ do
-          trace[Tactic.trans]"trying lemma {lem}"
-          let lemTy ← inferType (← mkConstWithLevelParams lem)
-          let arity ← withReducible <| forallTelescopeReducing lemTy fun es _ ↦ pure es.size
-          trace[Tactic.trans]"arity: {arity}"
-          trace[Tactic.trans]"lemma-type: {lemTy}"
-          let y ← (t'?.map (pure ·.1)).getD (mkFreshExprMVar none)
-          trace[Tactic.trans]"obtained y: {y}"
-          trace[Tactic.trans]"rel: {indentExpr rel}"
-          trace[Tactic.trans]"x:{indentExpr x}"
-          trace[Tactic.trans]"z:  {indentExpr z}"
-          let g₂ ← mkFreshExprMVar (some <| ← mkAppM' rel #[y, z]) .synthetic
-          trace[Tactic.trans]"obtained g₂: {g₂}"
-          let g₁ ← mkFreshExprMVar (some <| ← mkAppM' rel #[x, y]) .synthetic
-          trace[Tactic.trans]"obtained g₁: {g₁}"
-          g.assign (← mkAppOptM lem (mkArray (arity - 2) none ++ #[some g₁, some g₂]))
-          pure <| [g₁.mvarId!, g₂.mvarId!] ++ if let some (_, gs') := t'? then gs' else [y.mvarId!]
-        return
-      catch e =>
-        trace[Tactic.trans]"failed: {e.toMessageData}"
-        s.restore
-    throwError m!"no applicable transitivity lemma found for {indentExpr tgt}"
-
-syntax "transitivity" (ppSpace colGt term)? : tactic
-set_option hygiene false in
-macro_rules
-  | `(tactic| transitivity) => `(tactic| trans)
-  | `(tactic| transitivity $e) => `(tactic| trans $e)
-
-end Mathlib.Tactic
diff --git a/Mathlib/Tactic/ToAdditive/Frontend.lean b/Mathlib/Tactic/ToAdditive/Frontend.lean
index b4388a6778e84..c31b844975646 100644
--- a/Mathlib/Tactic/ToAdditive/Frontend.lean
+++ b/Mathlib/Tactic/ToAdditive/Frontend.lean
@@ -16,7 +16,7 @@ import Lean.Meta.Tactic.Rfl
 import Lean.Meta.Match.MatcherInfo
 import Batteries.Lean.NameMapAttribute
 import Batteries.Tactic.Lint -- useful to lint this file and for DiscrTree.elements
-import Mathlib.Tactic.Relation.Trans -- just to copy the attribute
+import Batteries.Tactic.Trans
 import Mathlib.Tactic.Eqns -- just to copy the attribute
 import Mathlib.Tactic.Simps.Basic
 
@@ -1167,7 +1167,7 @@ partial def applyAttributes (stx : Syntax) (rawAttrs : Array Syntax) (thisAttr s
       (fun b n => (b.tree.values.any fun t => t.declName = n)) thisAttr `ext src tgt
     warnAttr stx Lean.Meta.Rfl.reflExt (·.values.contains ·) thisAttr `refl src tgt
     warnAttr stx Lean.Meta.Symm.symmExt (·.values.contains ·) thisAttr `symm src tgt
-    warnAttr stx Mathlib.Tactic.transExt (·.values.contains ·) thisAttr `trans src tgt
+    warnAttr stx Batteries.Tactic.transExt (·.values.contains ·) thisAttr `trans src tgt
     warnAttr stx Lean.Meta.coeExt (·.contains ·) thisAttr `coe src tgt
     warnParametricAttr stx Lean.Linter.deprecatedAttr thisAttr `deprecated src tgt
     -- the next line also warns for `@[to_additive, simps]`, because of the application times
diff --git a/Mathlib/Tactic/Widget/CongrM.lean b/Mathlib/Tactic/Widget/CongrM.lean
index 9c259c3daaf30..dad4520d652cc 100644
--- a/Mathlib/Tactic/Widget/CongrM.lean
+++ b/Mathlib/Tactic/Widget/CongrM.lean
@@ -6,6 +6,7 @@ Authors: Patrick Massot
 
 import Mathlib.Tactic.Widget.SelectPanelUtils
 import Mathlib.Tactic.CongrM
+import Batteries.Lean.Position
 
 /-! # CongrM widget
 
diff --git a/Mathlib/Topology/Algebra/ProperAction/Basic.lean b/Mathlib/Topology/Algebra/ProperAction/Basic.lean
index fa7a99510f216..92fc69d56d9f4 100644
--- a/Mathlib/Topology/Algebra/ProperAction/Basic.lean
+++ b/Mathlib/Topology/Algebra/ProperAction/Basic.lean
@@ -118,7 +118,7 @@ theorem t2Space_quotient_mulAction_of_properSMul [ProperSMul G X] :
   · ext ⟨x₁, x₂⟩
     simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists,
       exists_eq_right]
-    rw [Quotient.eq_rel, MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
+    rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
   all_goals infer_instance
 
 /-- If a T2 group acts properly on a topological space, then this topological space is T2. -/
diff --git a/Mathlib/Topology/DiscreteQuotient.lean b/Mathlib/Topology/DiscreteQuotient.lean
index ed3253cad0993..bad892ec52aeb 100644
--- a/Mathlib/Topology/DiscreteQuotient.lean
+++ b/Mathlib/Topology/DiscreteQuotient.lean
@@ -69,7 +69,7 @@ variable {α X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [Topologic
 @[ext] -- Porting note: in Lean 4, uses projection to `r` instead of `Setoid`.
 structure DiscreteQuotient (X : Type*) [TopologicalSpace X] extends Setoid X where
   /-- For every point `x`, the set `{ y | Rel x y }` is an open set. -/
-  protected isOpen_setOf_rel : ∀ x, IsOpen (setOf (toSetoid.Rel x))
+  protected isOpen_setOf_rel : ∀ x, IsOpen (setOf (toSetoid x))
 
 namespace DiscreteQuotient
 
@@ -81,13 +81,13 @@ lemma toSetoid_injective : Function.Injective (@toSetoid X _)
 /-- Construct a discrete quotient from a clopen set. -/
 def ofIsClopen {A : Set X} (h : IsClopen A) : DiscreteQuotient X where
   toSetoid := ⟨fun x y => x ∈ A ↔ y ∈ A, fun _ => Iff.rfl, Iff.symm, Iff.trans⟩
-  isOpen_setOf_rel x := by by_cases hx : x ∈ A <;> simp [Setoid.Rel, hx, h.1, h.2, ← compl_setOf]
+  isOpen_setOf_rel x := by by_cases hx : x ∈ A <;> simp [hx, h.1, h.2, ← compl_setOf]
 
-theorem refl : ∀ x, S.Rel x x := S.refl'
+theorem refl : ∀ x, S.toSetoid x x := S.refl'
 
-theorem symm (x y : X) : S.Rel x y → S.Rel y x := S.symm'
+theorem symm (x y : X) : S.toSetoid x y → S.toSetoid y x := S.symm'
 
-theorem trans (x y z : X) : S.Rel x y → S.Rel y z → S.Rel x z := S.trans'
+theorem trans (x y z : X) : S.toSetoid x y → S.toSetoid y z → S.toSetoid x z := S.trans'
 
 /-- The setoid whose quotient yields the discrete quotient. -/
 add_decl_doc toSetoid
@@ -101,7 +101,7 @@ instance : TopologicalSpace S :=
 /-- The projection from `X` to the given discrete quotient. -/
 def proj : X → S := Quotient.mk''
 
-theorem fiber_eq (x : X) : S.proj ⁻¹' {S.proj x} = setOf (S.Rel x) :=
+theorem fiber_eq (x : X) : S.proj ⁻¹' {S.proj x} = setOf (S.toSetoid x) :=
   Set.ext fun _ => eq_comm.trans Quotient.eq''
 
 theorem proj_surjective : Function.Surjective S.proj :=
@@ -130,7 +130,7 @@ theorem isOpen_preimage (A : Set S) : IsOpen (S.proj ⁻¹' A) :=
 theorem isClosed_preimage (A : Set S) : IsClosed (S.proj ⁻¹' A) :=
   (S.isClopen_preimage A).1
 
-theorem isClopen_setOf_rel (x : X) : IsClopen (setOf (S.Rel x)) := by
+theorem isClopen_setOf_rel (x : X) : IsClopen (setOf (S.toSetoid x)) := by
   rw [← fiber_eq]
   apply isClopen_preimage
 
@@ -359,7 +359,7 @@ lemma comp_finsetClopens [CompactSpace X] :
     (Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ Finset.toSet) ∘
       finsetClopens X = fun ⟨f, _⟩ ↦ f.classes := by
   ext d
-  simp only [Setoid.classes, Setoid.Rel, Set.mem_setOf_eq, Function.comp_apply,
+  simp only [Setoid.classes, Set.mem_setOf_eq, Function.comp_apply,
     finsetClopens, Set.coe_toFinset, Set.mem_image, Set.mem_range,
     exists_exists_eq_and]
   constructor
diff --git a/Mathlib/Topology/MetricSpace/Contracting.lean b/Mathlib/Topology/MetricSpace/Contracting.lean
index 2fcec8e182a86..ac3f24a9253fa 100644
--- a/Mathlib/Topology/MetricSpace/Contracting.lean
+++ b/Mathlib/Topology/MetricSpace/Contracting.lean
@@ -137,7 +137,7 @@ theorem efixedPoint_eq_of_edist_lt_top (hf : ContractingWith K f) {x : α} (hx :
     efixedPoint f hf x hx = efixedPoint f hf y hy := by
   refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
     <;> try apply efixedPoint_isFixedPt
-  change edistLtTopSetoid.Rel _ _
+  change edistLtTopSetoid _ _
   trans x
   · apply Setoid.symm' -- Porting note: Originally `symm`
     exact hf.edist_efixedPoint_lt_top hx
@@ -221,7 +221,7 @@ theorem efixedPoint_eq_of_edist_lt_top' (hf : ContractingWith K f) {s : Set α}
     efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy := by
   refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
     <;> try apply efixedPoint_isFixedPt'
-  change edistLtTopSetoid.Rel _ _
+  change edistLtTopSetoid _ _
   trans x
   · apply Setoid.symm' -- Porting note: Originally `symm`
     apply edist_efixedPoint_lt_top'
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index 1ba06927812eb..d2e132acfed38 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -1632,7 +1632,7 @@ instance : TopologicalSpace (t2Quotient X) :=
 /-- The map from a topological space to its largest T2 quotient. -/
 def mk : X → t2Quotient X := Quotient.mk (t2Setoid X)
 
-lemma mk_eq {x y : X} : mk x = mk y ↔ ∀ s : Setoid X, T2Space (Quotient s) → s.Rel x y :=
+lemma mk_eq {x y : X} : mk x = mk y ↔ ∀ s : Setoid X, T2Space (Quotient s) → s x y :=
   Setoid.quotient_mk_sInf_eq
 
 variable (X)
diff --git a/scripts/noshake.json b/scripts/noshake.json
index d12c46a1821d1..b0c52f7471209 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -147,7 +147,6 @@
   "Mathlib.Tactic.Recover",
   "Mathlib.Tactic.ReduceModChar.Ext",
   "Mathlib.Tactic.Relation.Symm",
-  "Mathlib.Tactic.Relation.Trans",
   "Mathlib.Tactic.Rename",
   "Mathlib.Tactic.RenameBVar",
   "Mathlib.Tactic.Replace",
diff --git a/test/trans.lean b/test/trans.lean
deleted file mode 100644
index 50b5bc01e7b20..0000000000000
--- a/test/trans.lean
+++ /dev/null
@@ -1,109 +0,0 @@
-import Mathlib.Tactic.Relation.Trans
-import Mathlib.Tactic.GuardGoalNums
-
-set_option autoImplicit true
--- testing that the attribute is recognized and used
-def nleq (a b : Nat) : Prop := a ≤ b
-
-@[trans] def nleq_trans : nleq a b → nleq b c → nleq a c := Nat.le_trans
-
-example (a b c : Nat) : nleq a b → nleq b c → nleq a c := by
-  intro h₁ h₂
-  trans b
-  assumption
-  assumption
-
-example (a b c : Nat) : nleq a b → nleq b c → nleq a c := by intros; trans <;> assumption
-
--- using `Trans` typeclass
-@[trans] def eq_trans {a b c : α} : a = b → b = c → a = c := by
-  intro h₁ h₂
-  apply Eq.trans h₁ h₂
-
-example (a b c : Nat) : a = b → b = c → a = c := by intros; trans <;> assumption
-
-example (a b c : Nat) : a = b → b = c → a = c := by
-  intro h₁ h₂
-  trans b
-  assumption
-  assumption
-
-example : @Trans Nat Nat Nat (· ≤ ·) (· ≤ ·) (· ≤ ·) := inferInstance
-
-example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
-  intros h₁ h₂
-  trans ?b
-  case b => exact b
-  exact h₁
-  exact h₂
-
-example (a b c : α) (R : α → α → Prop) [Trans R R R] : R a b → R b c → R a c := by
-  intros h₁ h₂
-  trans ?b
-  case b => exact b
-  exact h₁
-  exact h₂
-
-example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
-  intros h₁ h₂
-  trans
-  exact h₁
-  exact h₂
-
-example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by intros; trans <;> assumption
-
-example (a b c : Nat) : a < b → b < c → a < c := by
-  intro h₁ h₂
-  trans b
-  assumption
-  assumption
-
-example (a b c : Nat) : a < b → b < c → a < c := by intros; trans <;> assumption
-
-example (x n p : Nat) (h₁ : n * Nat.succ p ≤ x) : n * p ≤ x := by
-  trans
-  · apply Nat.mul_le_mul_left; apply Nat.le_succ
-  · apply h₁
-
-example (a : α) (c : γ) : ∀ b : β, HEq a b → HEq b c → HEq a c := by
-    intro b h₁ h₂
-    trans b
-    assumption
-    assumption
-
-def MyLE (n m : Nat) := ∃ k, n + k = m
-
-@[trans] theorem MyLE.trans {n m k : Nat} (h1 : MyLE n m) (h2 : MyLE m k) : MyLE n k := by
-  cases h1
-  cases h2
-  subst_vars
-  exact ⟨_, Eq.symm <| Nat.add_assoc _ _ _⟩
-
-example {n m k : Nat} (h1 : MyLE n m) (h2 : MyLE m k) : MyLE n k := by
-  trans <;> assumption
-
-/-- `trans` for implications. -/
-example {A B C : Prop} (h : A → B) (g : B → C) : A → C := by
-  trans B
-  · guard_target =ₛ A → B -- ensure we have `B` and not a free metavariable.
-    exact h
-  · guard_target =ₛ B → C
-    exact g
-
-set_option linter.unusedTactic false in
-/-- `trans` for arrows between types. -/
-example {A B C : Type} (h : A → B) (g : B → C) : A → C := by
-  trans
-  guard_goal_nums 3 -- 3rd goal is the middle term
-  · exact h
-  · exact g
-
-universe u v w
-
-set_option linter.unusedTactic false in
-/-- `trans` for arrows between types. -/
-example {A : Type u} {B : Type v} {C : Type w} (h : A → B) (g : B → C) : A → C := by
-  trans
-  guard_goal_nums 3 -- 3rd goal is the middle term
-  · exact h
-  · exact g