diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
index 29d91b4ab7439..a7a16de103ee9 100644
--- a/Mathlib/Algebra/Algebra/Basic.lean
+++ b/Mathlib/Algebra/Algebra/Basic.lean
@@ -185,8 +185,7 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R}
     mpr := fun H =>
       H.symm ▸ by
         apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
-        erw [End_isUnit_apply_inv_apply_of_isUnit]
-        rfl }
+        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') }
 
 theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R}
     (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
@@ -195,8 +194,7 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R}
     mpr := fun H =>
       H.symm ▸ by
         apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
-        erw [End_isUnit_apply_inv_apply_of_isUnit]
-        rfl }
+        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm }
 
 end
 
diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
index 0d13d5ae72a71..2df0f53da5529 100644
--- a/Mathlib/Algebra/Group/Subgroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -69,7 +69,7 @@ Definitions in the file:
 * `MonoidHom.ker f` : the kernel of a group homomorphism `f` is the subgroup of elements `x : G`
   such that `f x = 1`
 
-* `MonoidHom.eq_locus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
+* `MonoidHom.eqLocus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
   `f x = g x` form a subgroup of `G`
 
 ## Implementation notes
diff --git a/Mathlib/Algebra/Lie/Subalgebra.lean b/Mathlib/Algebra/Lie/Subalgebra.lean
index 649208ace2362..a1d215735203f 100644
--- a/Mathlib/Algebra/Lie/Subalgebra.lean
+++ b/Mathlib/Algebra/Lie/Subalgebra.lean
@@ -224,7 +224,7 @@ variable [Module R M]
 `L`, we may regard `M` as a Lie module of `L'` by restriction. -/
 instance lieModule [LieModule R L M] : LieModule R L' M where
   smul_lie t x m := by
-    rw [coe_bracket_of_module]; erw [smul_lie]; simp only [coe_bracket_of_module]
+    rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
   lie_smul t x m := by simp only [coe_bracket_of_module, lie_smul]
 
 /-- An `L`-equivariant map of Lie modules `M → N` is `L'`-equivariant for any Lie subalgebra
diff --git a/Mathlib/Algebra/Module/Equiv/Basic.lean b/Mathlib/Algebra/Module/Equiv/Basic.lean
index 3d210451cac46..502f5ddd8ebdf 100644
--- a/Mathlib/Algebra/Module/Equiv/Basic.lean
+++ b/Mathlib/Algebra/Module/Equiv/Basic.lean
@@ -122,7 +122,7 @@ protected theorem smul_def (f : M ≃ₗ[R] M) (a : M) : f • a = f a :=
 
 /-- `LinearEquiv.applyDistribMulAction` is faithful. -/
 instance apply_faithfulSMul : FaithfulSMul (M ≃ₗ[R] M) M :=
-  ⟨@fun _ _ ↦ LinearEquiv.ext⟩
+  ⟨LinearEquiv.ext⟩
 
 instance apply_smulCommClass [SMul S R] [SMul S M] [IsScalarTower S R M] :
     SMulCommClass S (M ≃ₗ[R] M) M where
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
index c12393d6b86df..86b3f777ce844 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
@@ -553,8 +553,7 @@ lemma integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
   convert integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr
   refine _root_.integral_ofReal.symm.trans <| setIntegral_congr measurableSet_Ioi (fun t ht ↦ ?_)
   norm_cast
-  rw [← ofReal_cpow (le_of_lt ht), RCLike.ofReal_mul]
-  rfl
+  simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]
 
 open Lean.Meta Qq Mathlib.Meta.Positivity in
 /-- The `positivity` extension which identifies expressions of the form `Gamma a`. -/
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
index e0595d589e11d..e8e17232197f1 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
@@ -173,11 +173,9 @@ theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x := by
   let U := Ico 0 (π / 2)
   have intU : interior U = Ioo 0 (π / 2) := interior_Ico
   have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
-  have cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y := by
-    intro y hy
+  have cos_pos {y : ℝ} (hy : y ∈ U) : 0 < cos y := by
     exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
-  have sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y := by
-    intro y hy
+  have sin_pos {y : ℝ} (hy : y ∈ interior U) : 0 < sin y := by
     rw [intU] at hy
     exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
   have tan_cts_U : ContinuousOn tan U := by
@@ -186,8 +184,7 @@ theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x := by
     simp only [mem_setOf_eq]
     exact (cos_pos hz).ne'
   have tan_minus_id_cts : ContinuousOn (fun y : ℝ => tan y - y) U := tan_cts_U.sub continuousOn_id
-  have deriv_pos : ∀ y : ℝ, y ∈ interior U → 0 < deriv (fun y' : ℝ => tan y' - y') y := by
-    intro y hy
+  have deriv_pos (y : ℝ) (hy : y ∈ interior U) : 0 < deriv (fun y' : ℝ => tan y' - y') y := by
     have := cos_pos (interior_subset hy)
     simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
     norm_cast
diff --git a/Mathlib/FieldTheory/Finiteness.lean b/Mathlib/FieldTheory/Finiteness.lean
index 6c2e5621a9272..d6cc69e04c7ae 100644
--- a/Mathlib/FieldTheory/Finiteness.lean
+++ b/Mathlib/FieldTheory/Finiteness.lean
@@ -72,7 +72,7 @@ theorem coeSort_finsetBasisIndex [IsNoetherian K V] :
 /-- In a noetherian module over a division ring, there exists a finite basis.
 This is indexed by the `Finset` `IsNoetherian.finsetBasisIndex`.
 This is in contrast to the result `finite_basis_index (Basis.ofVectorSpace K V)`,
-which provides a set and a `Set.finite`.
+which provides a set and a `Set.Finite`.
 -/
 noncomputable def finsetBasis [IsNoetherian K V] : Basis (finsetBasisIndex K V) K V :=
   (Basis.ofVectorSpace K V).reindex (by rw [coeSort_finsetBasisIndex])
diff --git a/Mathlib/FieldTheory/Galois/Basic.lean b/Mathlib/FieldTheory/Galois/Basic.lean
index 868454440fa9b..56ce629fc2bea 100644
--- a/Mathlib/FieldTheory/Galois/Basic.lean
+++ b/Mathlib/FieldTheory/Galois/Basic.lean
@@ -24,7 +24,7 @@ In this file we define Galois extensions as extensions which are both separable
 
 - `IntermediateField.fixingSubgroup_fixedField` : If `E/F` is finite dimensional (but not
   necessarily Galois) then `fixingSubgroup (fixedField H) = H`
-- `IntermediateField.fixedField_fixingSubgroup`: If `E/F` is finite dimensional and Galois
+- `IsGalois.fixedField_fixingSubgroup`: If `E/F` is finite dimensional and Galois
   then `fixedField (fixingSubgroup K) = K`
 
 Together, these two results prove the Galois correspondence.
diff --git a/Mathlib/GroupTheory/MonoidLocalization/Basic.lean b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
index 988928ee6d456..b5db348da57a7 100644
--- a/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
+++ b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
@@ -548,7 +548,7 @@ theorem mk'_spec' (x) (y : S) : f.toMap y * f.mk' x y = f.toMap x := by rw [mul_
 
 @[to_additive]
 theorem eq_mk'_iff_mul_eq {x} {y : S} {z} : z = f.mk' x y ↔ z * f.toMap y = f.toMap x :=
-  ⟨fun H ↦ by rw [H, mk'_spec], fun H ↦ by erw [mul_inv_right, H]⟩
+  ⟨fun H ↦ by rw [H, mk'_spec], fun H ↦ by rw [mk', mul_inv_right, H]⟩
 
 @[to_additive]
 theorem mk'_eq_iff_eq_mul {x} {y : S} {z} : f.mk' x y = z ↔ f.toMap x = z * f.toMap y := by
@@ -773,9 +773,7 @@ theorem lift_comp : (f.lift hg).comp f.toMap = g := by ext; exact f.lift_eq hg _
 @[to_additive (attr := simp)]
 theorem lift_of_comp (j : N →* P) : f.lift (f.isUnit_comp j) = j := by
   ext
-  rw [lift_spec]
-  show j _ = j _ * _
-  erw [← j.map_mul, sec_spec']
+  simp_rw [lift_spec, MonoidHom.comp_apply, ← j.map_mul, sec_spec']
 
 @[to_additive]
 theorem epic_of_localizationMap {j k : N →* P} (h : ∀ a, j.comp f.toMap a = k.comp f.toMap a) :
@@ -834,8 +832,8 @@ theorem lift_surjective_iff :
     obtain ⟨z, hz⟩ := H v
     obtain ⟨x, hx⟩ := f.surj z
     use x
-    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2)]
-    erw [IsUnit.mul_liftRight_inv (g.restrict S) hg, mul_one]
+    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
+      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, mul_one]
   · intro H v
     obtain ⟨x, hx⟩ := H v
     use f.mk' x.1 x.2
@@ -1131,9 +1129,9 @@ of `AddCommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`."]
 def ofMulEquivOfLocalizations (k : N ≃* P) : LocalizationMap S P :=
   (k.toMonoidHom.comp f.toMap).toLocalizationMap (fun y ↦ isUnit_comp f k.toMonoidHom y)
     (fun v ↦
-      let ⟨z, hz⟩ := k.toEquiv.surjective v
+      let ⟨z, hz⟩ := k.surjective v
       let ⟨x, hx⟩ := f.surj z
-      ⟨x, show v * k _ = k _ by rw [← hx, map_mul, ← hz]; rfl⟩)
+      ⟨x, show v * k _ = k _ by rw [← hx, map_mul, ← hz]⟩)
     fun x y ↦ (k.apply_eq_iff_eq.trans f.eq_iff_exists).1
 
 @[to_additive (attr := simp)]
@@ -1203,18 +1201,17 @@ def ofMulEquivOfDom {k : P ≃* M} (H : T.map k.toMonoidHom = S) : LocalizationM
       ⟨z, hz⟩)
     (fun z ↦
       let ⟨x, hx⟩ := f.surj z
-      let ⟨v, hv⟩ := k.toEquiv.surjective x.1
-      let ⟨w, hw⟩ := k.toEquiv.surjective x.2
-      ⟨(v, ⟨w, H' ▸ show k w ∈ S from hw.symm ▸ x.2.2⟩),
-        show z * f.toMap (k.toEquiv w) = f.toMap (k.toEquiv v) by erw [hv, hw, hx]⟩)
-    fun x y ↦
-    show f.toMap _ = f.toMap _ → _ by
-      erw [f.eq_iff_exists]
-      exact
-        fun ⟨c, hc⟩ ↦
-          let ⟨d, hd⟩ := k.toEquiv.surjective c
-          ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, by
-            erw [← hd, ← map_mul k, ← map_mul k] at hc; exact k.toEquiv.injective hc⟩
+      let ⟨v, hv⟩ := k.surjective x.1
+      let ⟨w, hw⟩ := k.surjective x.2
+      ⟨(v, ⟨w, H' ▸ show k w ∈ S from hw.symm ▸ x.2.2⟩), by
+        simp_rw [MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, hv, hw, hx]⟩)
+    fun x y ↦ by
+      rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe,
+        MonoidHom.coe_coe, f.eq_iff_exists]
+      rintro ⟨c, hc⟩
+      let ⟨d, hd⟩ := k.surjective c
+      refine ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩
+      rw [← hd, ← map_mul k, ← map_mul k] at hc; exact k.injective hc
 
 @[to_additive (attr := simp)]
 theorem ofMulEquivOfDom_apply {k : P ≃* M} (H : T.map k.toMonoidHom = S) (x) :
diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
index bba76de12bd95..ed68d3b7b7e44 100644
--- a/Mathlib/LinearAlgebra/LinearIndependent.lean
+++ b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -591,8 +591,7 @@ theorem LinearIndependent.units_smul {v : ι → M} (hv : LinearIndependent R v)
     exact (hgs i hi).symm ▸ zero_smul _ _
   · rw [← hsum, Finset.sum_congr rfl _]
     intros
-    erw [Pi.smul_apply, smul_assoc]
-    rfl
+    rw [Pi.smul_apply', smul_assoc, Units.smul_def]
 
 lemma LinearIndependent.eq_of_pair {x y : M} (h : LinearIndependent R ![x, y])
     {s t s' t' : R} (h' : s • x + t • y = s' • x + t' • y) : s = s' ∧ t = t' := by
diff --git a/Mathlib/Logic/Function/FiberPartition.lean b/Mathlib/Logic/Function/FiberPartition.lean
index e82895e5b975f..e1463b5d0e46b 100644
--- a/Mathlib/Logic/Function/FiberPartition.lean
+++ b/Mathlib/Logic/Function/FiberPartition.lean
@@ -62,7 +62,7 @@ lemma fiber_nonempty (f : Y → Z) (a : Fiber f) : Set.Nonempty a.val := by
   rw [mem_iff_eq_image, ← map_preimage_eq_image]
 
 lemma map_preimage_eq_image_map {W : Type*} (f : Y → Z) (g : Z → W) (a : Fiber (g ∘ f)) :
-    g (f a.preimage) = a.image := by rw [← map_preimage_eq_image]; rfl
+    g (f a.preimage) = a.image := by rw [← map_preimage_eq_image, comp_apply]
 
 lemma image_eq_image_mk (f : Y → Z) (g : X → Y) (a : Fiber (f ∘ g)) :
     a.image = (Fiber.mk f (g (a.preimage _))).image := by
diff --git a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
index db051f36a5bc3..0d8110dc76977 100644
--- a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
+++ b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
@@ -127,10 +127,10 @@ theorem LocallyIntegrableOn.aestronglyMeasurable [SecondCountableTopology X]
   rw [this, aestronglyMeasurable_iUnion_iff]
   exact fun i : ℕ => (hu i).aestronglyMeasurable
 
-/-- If `s` is either open, or closed, then `f` is locally integrable on `s` iff it is integrable on
-every compact subset contained in `s`. -/
+/-- If `s` is locally closed (e.g. open or closed), then `f` is locally integrable on `s` iff it is
+integrable on every compact subset contained in `s`. -/
 theorem locallyIntegrableOn_iff [LocallyCompactSpace X] (hs : IsLocallyClosed s) :
-    LocallyIntegrableOn f s μ ↔ ∀ (k : Set X), k ⊆ s → (IsCompact k → IntegrableOn f k μ) := by
+    LocallyIntegrableOn f s μ ↔ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k μ := by
   refine ⟨fun hf k hk ↦ hf.integrableOn_compact_subset hk, fun hf x hx ↦ ?_⟩
   rcases hs with ⟨U, Z, hU, hZ, rfl⟩
   rcases exists_compact_subset hU hx.1 with ⟨K, hK, hxK, hKU⟩
diff --git a/Mathlib/MeasureTheory/Measure/SeparableMeasure.lean b/Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
index a475581af381f..55e3abb732208 100644
--- a/Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
@@ -32,7 +32,7 @@ of separability in the metric space made by constant indicators equipped with th
 
 ## Main definitions
 
-* `MeasureTheory.Measure.μ.MeasureDense 𝒜`: `𝒜` is a measure-dense family if it only contains
+* `MeasureTheory.Measure.MeasureDense μ 𝒜`: `𝒜` is a measure-dense family if it only contains
   measurable sets and if the following condition is satisfied: if `s` is measurable with finite
   measure, then for any `ε > 0` there exists `t ∈ 𝒜` such that `μ (s ∆ t) < ε `.
 * `MeasureTheory.IsSeparable`: A measure is separable if there exists a countable and
@@ -87,8 +87,7 @@ structure Measure.MeasureDense (μ : Measure X) (𝒜 : Set (Set X)) : Prop :=
   /-- Each set has to be measurable. -/
   measurable : ∀ s ∈ 𝒜, MeasurableSet s
   /-- Any measurable set can be approximated by sets in the family. -/
-  approx : ∀ s, MeasurableSet s → μ s ≠ ∞ → ∀ (ε : ℝ),
-    0 < ε → ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε
+  approx : ∀ s, MeasurableSet s → μ s ≠ ∞ → ∀ ε : ℝ, 0 < ε → ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε
 
 theorem Measure.MeasureDense.nonempty (h𝒜 : μ.MeasureDense 𝒜) : 𝒜.Nonempty := by
   rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by norm_num) with ⟨t, ht, -⟩
@@ -103,8 +102,8 @@ theorem Measure.MeasureDense.nonempty' (h𝒜 : μ.MeasureDense 𝒜) :
 
 /-- The set of measurable sets is measure-dense. -/
 theorem measureDense_measurableSet : μ.MeasureDense {s | MeasurableSet s} where
-  measurable := fun _ h ↦ h
-  approx := fun s hs _ ε ε_pos ↦ ⟨s, hs, by simpa⟩
+  measurable _ h := h
+  approx s hs _ ε ε_pos := ⟨s, hs, by simpa⟩
 
 /-- If a family of sets `𝒜` is measure-dense in `X`, then any measurable set with finite measure
 can be approximated by sets in `𝒜` with finite measure. -/
@@ -155,9 +154,8 @@ theorem Measure.MeasureDense.indicatorConstLp_subset_closure (h𝒜 : μ.Measure
 with finite measure. -/
 theorem Measure.MeasureDense.fin_meas (h𝒜 : μ.MeasureDense 𝒜) :
     μ.MeasureDense {s | s ∈ 𝒜 ∧ μ s ≠ ∞} where
-  measurable := fun s h ↦ h𝒜.measurable s h.1
-  approx := by
-    intro s ms hμs ε ε_pos
+  measurable s h := h𝒜.measurable s h.1
+  approx s ms hμs ε ε_pos := by
     rcases Measure.MeasureDense.fin_meas_approx h𝒜 ms hμs ε ε_pos with ⟨t, t_mem, hμt, hμst⟩
     exact ⟨t, ⟨t_mem, hμt⟩, hμst⟩
 
@@ -165,12 +163,11 @@ theorem Measure.MeasureDense.fin_meas (h𝒜 : μ.MeasureDense 𝒜) :
 this algebra of sets is measure-dense. -/
 theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite [IsFiniteMeasure μ]
     (h𝒜 : IsSetAlgebra 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) : μ.MeasureDense 𝒜 where
-  measurable := fun s hs ↦ hgen ▸ measurableSet_generateFrom hs
-  approx := by
+  measurable s hs := hgen ▸ measurableSet_generateFrom hs
+  approx s ms := by
     -- We want to show that any measurable set can be approximated by sets in `𝒜`. To do so, it is
     -- enough to show that such sets constitute a `σ`-algebra containing `𝒜`. This is contained in
     -- the theorem `generateFrom_induction`.
-    intro s ms
     have : MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (s ∆ t)).toReal < ε := by
       apply generateFrom_induction
         (p := fun s ↦ MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (s ∆ t)).toReal < ε)
@@ -220,14 +217,14 @@ theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite [IsFiniteMeasur
                 apply _root_.add_lt_add
                 · rw [measure_diff (h_fin := measure_ne_top _ _),
                     toReal_sub_of_le (ha := measure_ne_top _ _)]
-                  apply lt_of_le_of_lt (sub_le_dist ..)
-                  simp only [Finset.mem_range, Nat.lt_add_one_iff]
-                  exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
-                  exact (measure_mono <| iUnion_subset <|
-                    fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i))
-                  exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)
-                  exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
-                    (fun n _ ↦ (hf n).1.nullMeasurableSet)
+                  · apply lt_of_le_of_lt (sub_le_dist ..)
+                    simp only [Finset.mem_range, Nat.lt_add_one_iff]
+                    exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
+                  · exact measure_mono <| iUnion_subset <|
+                      fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i
+                  · exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)
+                  · exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
+                      (fun n _ ↦ (hf n).1.nullMeasurableSet)
                 · calc
                     (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
                     (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal
@@ -257,18 +254,17 @@ theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite (h𝒜 : I
     (S : μ.FiniteSpanningSetsIn 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) :
     μ.MeasureDense 𝒜 where
   measurable s hs := hgen ▸ measurableSet_generateFrom hs
-  approx := by
+  approx s ms hμs ε ε_pos := by
     -- We use partial unions of (Sₙ) to get a monotone family spanning `X`.
     let T := Accumulate S.set
-    have T_mem : ∀ n, T n ∈ 𝒜 := fun n ↦ by
+    have T_mem (n) : T n ∈ 𝒜 := by
       simpa using h𝒜.biUnion_mem {k | k ≤ n}.toFinset (fun k _ ↦ S.set_mem k)
-    have T_finite : ∀ n, μ (T n) < ∞ := fun n ↦ by
+    have T_finite (n) : μ (T n) < ∞ := by
       simpa using measure_biUnion_lt_top {k | k ≤ n}.toFinset.finite_toSet
         (fun k _ ↦ S.finite k)
     have T_spanning : ⋃ n, T n = univ := S.spanning ▸ iUnion_accumulate
     -- We use the fact that we already know this is true for finite measures. As `⋃ n, T n = X`,
     -- we have that `μ ((T n) ∩ s) ⟶ μ s`.
-    intro s ms hμs ε ε_pos
     have mono : Monotone (fun n ↦ (T n) ∩ s) := fun m n hmn ↦ inter_subset_inter_left s
         (biUnion_subset_biUnion_left fun k hkm ↦ Nat.le_trans hkm hmn)
     have := tendsto_measure_iUnion_atTop (μ := μ) mono
@@ -423,15 +419,14 @@ instance Lp.SecondCountableTopology [IsSeparable μ] [TopologicalSpace.Separable
   -- constant indicators with support in `𝒜₀`, and is denoted `D`. To make manipulations easier,
   -- we define the function `key` which given an integer `n` and two families of `n` elements
   -- in `u` and `𝒜₀` associates the corresponding sum.
-  let key : (n : ℕ) → (Fin n → u) → (Fin n → 𝒜₀) → (Lp E p μ) :=
-    fun n d s ↦ ∑ i, indicatorConstLp p (h𝒜₀.measurable (s i) (Subtype.mem (s i)))
-      (s i).2.2 (d i : E)
+  let key (n : ℕ) (d : Fin n → u) (s : Fin n → 𝒜₀) : (Lp E p μ) :=
+    ∑ i, indicatorConstLp p (h𝒜₀.measurable (s i) (Subtype.mem (s i))) (s i).2.2 (d i : E)
   let D := {s : Lp E p μ | ∃ n d t, s = key n d t}
   refine ⟨D, ?_, ?_⟩
   · -- Countability directly follows from countability of `u` and `𝒜₀`. The function `f` below
     -- is the uncurryfied version of `key`, which is easier to manipulate as countability of the
     -- domain is automatically infered.
-    let f : (Σ n : ℕ, (Fin n → u) × (Fin n → 𝒜₀)) → Lp E p μ := fun nds ↦ key nds.1 nds.2.1 nds.2.2
+    let f (nds : Σ n : ℕ, (Fin n → u) × (Fin n → 𝒜₀)) : Lp E p μ := key nds.1 nds.2.1 nds.2.2
     have := count_𝒜₀.to_subtype
     have := countable_u.to_subtype
     have : D ⊆ range f := by
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 8e0ff1ca52eca..5970d297810cb 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -613,7 +613,7 @@ theorem mem_span_latticeBasis (x : (mixedSpace K)) :
   rfl
 
 theorem span_latticeBasis :
-    (Submodule.span ℤ (Set.range (latticeBasis K))) = (mixedEmbedding.integerLattice K) :=
+    Submodule.span ℤ (Set.range (latticeBasis K)) = mixedEmbedding.integerLattice K :=
   Submodule.ext_iff.mpr (mem_span_latticeBasis K)
 
 instance : DiscreteTopology (mixedEmbedding.integerLattice K) := by
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
index f9b153340e1c4..223002432594b 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
@@ -250,22 +250,22 @@ variable (K) in
 /-- The set of images by `mixedEmbedding` of algebraic integers of `K` contained in the
 fundamental cone. -/
 def integralPoint : Set (mixedSpace K) :=
-  fundamentalCone K ∩ (mixedEmbedding.integerLattice K)
+  fundamentalCone K ∩ mixedEmbedding.integerLattice K
 
 theorem mem_integralPoint {a : mixedSpace K} :
-    a ∈ integralPoint K ↔ a ∈ fundamentalCone K ∧ ∃ x : (𝓞 K), mixedEmbedding K x = a:= by
+    a ∈ integralPoint K ↔ a ∈ fundamentalCone K ∧ ∃ x : 𝓞 K, mixedEmbedding K x = a := by
   simp only [integralPoint, Set.mem_inter_iff, SetLike.mem_coe, LinearMap.mem_range,
     AlgHom.toLinearMap_apply, RingHom.toIntAlgHom_coe, RingHom.coe_comp, Function.comp_apply]
 
 /-- If `a` is an integral point, then there is a *unique* algebraic integer in `𝓞 K` such
 that `mixedEmbedding K x = a`. -/
 theorem exists_unique_preimage_of_integralPoint {a : mixedSpace K} (ha : a ∈ integralPoint K) :
-    ∃! x : (𝓞 K), mixedEmbedding K x = a := by
+    ∃! x : 𝓞 K, mixedEmbedding K x = a := by
   obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integralPoint.mp ha
   refine Function.Injective.existsUnique_of_mem_range ?_ (Set.mem_range_self x)
   exact (mixedEmbedding_injective K).comp RingOfIntegers.coe_injective
 
-theorem integralPoint_ne_zero (a : integralPoint K) :  (a : mixedSpace K) ≠ 0 := by
+theorem integralPoint_ne_zero (a : integralPoint K) : (a : mixedSpace K) ≠ 0 := by
   by_contra!
   exact a.prop.1.2 (this.symm ▸ mixedEmbedding.norm.map_zero')
 
diff --git a/Mathlib/Probability/Distributions/Gamma.lean b/Mathlib/Probability/Distributions/Gamma.lean
index 0548d04bfd3c0..562c9b3c3b6f9 100644
--- a/Mathlib/Probability/Distributions/Gamma.lean
+++ b/Mathlib/Probability/Distributions/Gamma.lean
@@ -30,8 +30,8 @@ open MeasureTheory Real Set Filter Topology
 lemma lintegral_Iic_eq_lintegral_Iio_add_Icc {y z : ℝ} (f : ℝ → ℝ≥0∞) (hzy : z ≤ y) :
     ∫⁻ x in Iic y, f x = (∫⁻ x in Iio z, f x) + ∫⁻ x in Icc z y, f x := by
   rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc]
-  rw [Set.disjoint_iff]
-  rintro x ⟨h1 : x < _, h2, _⟩
+  simp_rw [Set.disjoint_iff_forall_ne, mem_Iio, mem_Icc]
+  intros
   linarith
 
 namespace ProbabilityTheory
@@ -49,8 +49,9 @@ def gammaPDF (a r x : ℝ) : ℝ≥0∞ :=
   ENNReal.ofReal (gammaPDFReal a r x)
 
 lemma gammaPDF_eq (a r x : ℝ) :
-    gammaPDF a r x = ENNReal.ofReal (if 0 ≤ x then
-    r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x)) else 0) := rfl
+    gammaPDF a r x =
+      ENNReal.ofReal (if 0 ≤ x then r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x)) else 0) :=
+  rfl
 
 lemma gammaPDF_of_neg {a r x : ℝ} (hx : x < 0) : gammaPDF a r x = 0 := by
   simp only [gammaPDF_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero]
diff --git a/Mathlib/RingTheory/MvPowerSeries/LexOrder.lean b/Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
index aaab1b9cc3f6b..f5472cc79ef0c 100644
--- a/Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
+++ b/Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
@@ -104,13 +104,10 @@ theorem le_lexOrder_iff {φ : MvPowerSeries σ R} {w : WithTop (Lex (σ →₀ 
     intro h'
     have hφ : φ ≠ 0 := by
       rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]
-      intro h''
-      rw [h'', ← not_le] at h'
-      apply h'
-      exact le_top
+      exact ne_top_of_lt h'
     obtain ⟨d, hd⟩ := exists_finsupp_eq_lexOrder_of_ne_zero hφ
     refine coeff_ne_zero_of_lexOrder hd.symm (h d ?_)
-    exact (lt_of_eq_of_lt hd.symm h')
+    rwa [← hd]
 
 theorem min_lexOrder_le {φ ψ : MvPowerSeries σ R} :
     min (lexOrder φ) (lexOrder ψ) ≤ lexOrder (φ + ψ)  := by
diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean
index edce0ce9c8677..f1887c8c8f025 100644
--- a/Mathlib/RingTheory/UniqueFactorizationDomain.lean
+++ b/Mathlib/RingTheory/UniqueFactorizationDomain.lean
@@ -323,8 +323,7 @@ theorem WfDvdMonoid.of_exists_prime_factors : WfDvdMonoid α :=
       rw [dif_neg ane0]
       by_cases h : b = 0
       · simp [h, lt_top_iff_ne_top]
-      · rw [dif_neg h]
-        erw [WithTop.coe_lt_coe]
+      · rw [dif_neg h, Nat.cast_lt]
         have cne0 : c ≠ 0 := by
           refine mt (fun con => ?_) h
           rw [b_eq, con, mul_zero]
@@ -390,8 +389,8 @@ theorem MulEquiv.uniqueFactorizationMonoid (e : α ≃* β) (hα : UniqueFactori
         he ▸ e.prime_iff.1 (hp c hc),
         Units.map e.toMonoidHom u,
       by
-        erw [Multiset.prod_hom, ← map_mul e, h]
-        simp⟩
+        rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
+          apply_symm_apply]⟩
 
 theorem MulEquiv.uniqueFactorizationMonoid_iff (e : α ≃* β) :
     UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β :=
diff --git a/Mathlib/Topology/FiberPartition.lean b/Mathlib/Topology/FiberPartition.lean
index c01b90f3fe77b..8e21ee229b9e1 100644
--- a/Mathlib/Topology/FiberPartition.lean
+++ b/Mathlib/Topology/FiberPartition.lean
@@ -29,7 +29,7 @@ variable [TopologicalSpace S]
 /-- The canonical map from the disjoint union induced by `f` to `S`. -/
 @[simps apply]
 def sigmaIsoHom : C((x : Fiber f) × x.val, S) where
-  toFun := fun ⟨a, x⟩ ↦ x.val
+  toFun | ⟨a, x⟩ => x.val
 
 lemma sigmaIsoHom_inj : Function.Injective (sigmaIsoHom f) := by
   rintro ⟨⟨_, _, rfl⟩, ⟨_, hx⟩⟩ ⟨⟨_, _, rfl⟩, ⟨_, hy⟩⟩ h
@@ -43,7 +43,7 @@ lemma sigmaIsoHom_surj : Function.Surjective (sigmaIsoHom f) :=
 
 /-- The inclusion map from a component of the disjoint union induced by `f` into `S`. -/
 def sigmaIncl (a : Fiber f) : C(a.val, S) where
-  toFun := fun x ↦ x.val
+  toFun x := x.val
 
 /-- The inclusion map from a fiber of a composition into the intermediate fiber. -/
 def sigmaInclIncl {X : Type*} (g : Y → X) (a : Fiber (g ∘ f))
@@ -53,7 +53,7 @@ def sigmaInclIncl {X : Type*} (g : Y → X) (a : Fiber (g ∘ f))
     have := x.prop
     simp only [sigmaIncl, ContinuousMap.coe_mk, Fiber.mem_iff_eq_image, comp_apply] at this
     rw [Fiber.mem_iff_eq_image, Fiber.mk_image, this, ← Fiber.map_preimage_eq_image]
-    rfl⟩
+    simp [sigmaIncl]⟩
 
 variable (l : LocallyConstant S Y) [CompactSpace S]