diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean
index 0903a38197e0a..3a2ba186ae171 100644
--- a/Mathlib/Algebra/Algebra/Hom.lean
+++ b/Mathlib/Algebra/Algebra/Hom.lean
@@ -73,10 +73,10 @@ instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass
 /-- Turn an element of a type `F` satisfying `AlgHomClass F α β` into an actual
 `AlgHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
 @[coe]
-def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B :=
-  { (f : A →+* B) with
-      toFun := f
-      commutes' := AlgHomClass.commutes f }
+def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B where
+  __ := (f : A →+* B)
+  toFun := f
+  commutes' := AlgHomClass.commutes f
 
 instance coeTC {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
   ⟨AlgHomClass.toAlgHom⟩
diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
index 7cd2933b52afd..f390081d3ec26 100644
--- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
+++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@@ -620,14 +620,12 @@ def rangeRestrict (f : A →ₐ[R] B) : A →ₐ[R] f.range :=
   f.codRestrict f.range f.mem_range_self
 #align alg_hom.range_restrict AlgHom.rangeRestrict
 
-theorem rangeRestrict_surjective (f : A →ₐ[R] B):
-    Function.Surjective (f.rangeRestrict) :=
+theorem rangeRestrict_surjective (f : A →ₐ[R] B) : Function.Surjective (f.rangeRestrict) :=
   fun ⟨_y, hy⟩ =>
-  let ⟨x, hx⟩ := hy
-  ⟨x, SetCoe.ext hx⟩
+    let ⟨x, hx⟩ := hy
+    ⟨x, SetCoe.ext hx⟩
 
-theorem ker_rangeRestrict (f : A →ₐ[R] B) :
-    RingHom.ker f.rangeRestrict = RingHom.ker f :=
+theorem ker_rangeRestrict (f : A →ₐ[R] B) : RingHom.ker f.rangeRestrict = RingHom.ker f :=
   Ideal.ext fun _ ↦ Subtype.ext_iff
 
 /-- The equalizer of two R-algebra homomorphisms -/
diff --git a/Mathlib/Algebra/Module/CharacterModule.lean b/Mathlib/Algebra/Module/CharacterModule.lean
index 07e9d58d4030b..42e0c798e313e 100644
--- a/Mathlib/Algebra/Module/CharacterModule.lean
+++ b/Mathlib/Algebra/Module/CharacterModule.lean
@@ -153,8 +153,10 @@ by the ideal generated by the order of `a`. -/
     (ℤ ∙ a) ≃ₗ[ℤ] ℤ ⧸ Ideal.span {(addOrderOf a : ℤ)} :=
   LinearEquiv.ofEq _ _ (LinearMap.span_singleton_eq_range ℤ A a) ≪≫ₗ
   (LinearMap.quotKerEquivRange <| LinearMap.toSpanSingleton ℤ A a).symm ≪≫ₗ
-  Submodule.quotEquivOfEq _ _
-    (by ext1 x; rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero]; rfl)
+  Submodule.quotEquivOfEq _ _ (by
+    ext1 x
+    rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
+      LinearMap.toSpanSingleton_apply])
 
 lemma intSpanEquivQuotAddOrderOf_apply_self (a : A) :
     intSpanEquivQuotAddOrderOf a ⟨a, Submodule.mem_span_singleton_self a⟩ =
diff --git a/Mathlib/Algebra/Order/Nonneg/Ring.lean b/Mathlib/Algebra/Order/Nonneg/Ring.lean
index 0e4913a0bab60..d24d01aae04a1 100644
--- a/Mathlib/Algebra/Order/Nonneg/Ring.lean
+++ b/Mathlib/Algebra/Order/Nonneg/Ring.lean
@@ -220,7 +220,7 @@ instance addMonoidWithOne [OrderedSemiring α] : AddMonoidWithOne { x : α // 0
     Nonneg.orderedAddCommMonoid with
     natCast := fun n => ⟨n, Nat.cast_nonneg n⟩
     natCast_zero := by simp
-    natCast_succ := fun _ => by simp only [Nat.cast_add, Nat.cast_one]; rfl }
+    natCast_succ := fun _ => by ext; simp }
 #align nonneg.add_monoid_with_one Nonneg.addMonoidWithOne
 
 @[simp, norm_cast]
diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
index 68f6d4199db1c..d79d7c084b5d2 100644
--- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
+++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
@@ -685,7 +685,7 @@ lemma fromSpec_toSpec {f : A} {m : ℕ} (hm : 0 < m) (f_deg : f ∈ 𝒜 m) (x :
   · intro i
     erw [ToSpec.mem_carrier_iff, HomogeneousLocalization.val_mk'']
     dsimp only [GradedAlgebra.proj_apply]
-    rw [show (mk (decompose 𝒜 z i ^ m) ⟨f^i, ⟨i, rfl⟩⟩: Away f) =
+    rw [show (mk (decompose 𝒜 z i ^ m) ⟨f^i, ⟨i, rfl⟩⟩ : Away f) =
       (decompose 𝒜 z i ^ m : A) • (mk 1 ⟨f^i, ⟨i, rfl⟩⟩ : Away f) by
       · rw [smul_mk, smul_eq_mul, mul_one], Algebra.smul_def]
     exact Ideal.mul_mem_right _ _ <|
diff --git a/Mathlib/Analysis/Asymptotics/Asymptotics.lean b/Mathlib/Analysis/Asymptotics/Asymptotics.lean
index 3d670eca940e6..9ced5a255ac8c 100644
--- a/Mathlib/Analysis/Asymptotics/Asymptotics.lean
+++ b/Mathlib/Analysis/Asymptotics/Asymptotics.lean
@@ -1984,7 +1984,7 @@ theorem isBigOWith_of_eq_mul {u v : α → R} (φ : α → R) (hφ : ∀ᶠ x in
 #align asymptotics.is_O_with_of_eq_mul Asymptotics.isBigOWith_of_eq_mul
 
 theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :
-    IsBigOWith c l u v ↔ ∃ (φ : α → 𝕜) (_hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c), u =ᶠ[l] φ * v := by
+    IsBigOWith c l u v ↔ ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v := by
   constructor
   · intro h
     use fun x => u x / v x
@@ -1995,12 +1995,12 @@ theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :
 #align asymptotics.is_O_with_iff_exists_eq_mul Asymptotics.isBigOWith_iff_exists_eq_mul
 
 theorem IsBigOWith.exists_eq_mul (h : IsBigOWith c l u v) (hc : 0 ≤ c) :
-    ∃ (φ : α → 𝕜) (_hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c), u =ᶠ[l] φ * v :=
+    ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v :=
   (isBigOWith_iff_exists_eq_mul hc).mp h
 #align asymptotics.is_O_with.exists_eq_mul Asymptotics.IsBigOWith.exists_eq_mul
 
 theorem isBigO_iff_exists_eq_mul :
-    u =O[l] v ↔ ∃ (φ : α → 𝕜) (_hφ : l.IsBoundedUnder (· ≤ ·) (norm ∘ φ)), u =ᶠ[l] φ * v := by
+    u =O[l] v ↔ ∃ φ : α → 𝕜, l.IsBoundedUnder (· ≤ ·) (norm ∘ φ) ∧ u =ᶠ[l] φ * v := by
   constructor
   · rintro h
     rcases h.exists_nonneg with ⟨c, hnnc, hc⟩
@@ -2014,7 +2014,7 @@ alias ⟨IsBigO.exists_eq_mul, _⟩ := isBigO_iff_exists_eq_mul
 #align asymptotics.is_O.exists_eq_mul Asymptotics.IsBigO.exists_eq_mul
 
 theorem isLittleO_iff_exists_eq_mul :
-    u =o[l] v ↔ ∃ (φ : α → 𝕜) (_hφ : Tendsto φ l (𝓝 0)), u =ᶠ[l] φ * v := by
+    u =o[l] v ↔ ∃ φ : α → 𝕜, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v := by
   constructor
   · exact fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩
   · simp only [IsLittleO_def]
diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
index d65467bee70a7..0935d121f7c5b 100644
--- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
+++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
@@ -151,15 +151,10 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
     rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
       sq, ← div_div, ← div_div, ← div_div, div_mul_cancel _ (norm_eq_zero.not.mpr hw_ne)]
   --* Rewrite integral in terms of `f v - f (v + w')`.
-  -- Porting note: this was
-  -- rw [norm_eq_abs, ← Complex.ofReal_one, ← ofReal_bit0, ← of_real_div,
-  --   Complex.abs_of_nonneg one_half_pos.le]
-  have : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by norm_num
+  have : ‖(1 / 2 : ℂ)‖ = 2⁻¹ := by norm_num
   rw [fourier_integral_eq_half_sub_half_period_translate hw_ne
       (hf1.integrable_of_hasCompactSupport hf2),
-    norm_smul, this]
-  have : ε = 1 / 2 * (2 * ε) := by field_simp; rw [mul_comm]
-  rw [this, mul_lt_mul_left (one_half_pos : (0 : ℝ) < 1 / 2)]
+    norm_smul, this, inv_mul_eq_div, div_lt_iff' two_pos]
   refine' lt_of_le_of_lt (norm_integral_le_integral_norm _) _
   simp_rw [norm_smul, norm_eq_abs, abs_coe_circle, one_mul]
   --* Show integral can be taken over A only.
@@ -176,7 +171,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
       refine' (div_le_one <| norm_pos_iff.mpr hw_ne).mpr _
       refine' le_trans (le_add_of_nonneg_right <| one_div_nonneg.mpr <| _) hw_bd
       exact (mul_pos (zero_lt_two' ℝ) hδ1).le
-    · exact ((le_add_iff_nonneg_right _).mpr zero_le_one).trans hv.le
+    · exact (le_add_of_nonneg_right zero_le_one).trans hv.le
   rw [int_A]; clear int_A
   --* Bound integral using fact that `‖f v - f (v + w')‖` is small.
   have bdA : ∀ v : V, v ∈ A → ‖‖f v - f (v + i w)‖‖ ≤ ε / B := by
@@ -185,10 +180,9 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
     refine' fun x _ => (hδ2 _).le
     rw [sub_add_cancel', norm_neg, hw'_nm, ← div_div, div_lt_iff (norm_pos_iff.mpr hw_ne), ←
       div_lt_iff' hδ1, div_div]
-    refine' (lt_add_of_pos_left _ _).trans_le hw_bd
-    exact one_half_pos
+    exact (lt_add_of_pos_left _ one_half_pos).trans_le hw_bd
   have bdA2 := norm_set_integral_le_of_norm_le_const (hB_vol.trans_lt ENNReal.coe_lt_top) bdA ?_
-  swap;
+  swap
   · apply Continuous.aestronglyMeasurable
     exact
       continuous_norm.comp <|
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
index 74e3f1188f371..6069a1c6a6624 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
@@ -62,10 +62,12 @@ lemma one_sub_sq_div_two_le_cos : 1 - x ^ 2 / 2 ≤ cos x := by
   · simpa using this $ neg_nonneg.2 $ le_of_not_le hx₀
   suffices MonotoneOn (fun x ↦ cos x + x ^ 2 / 2) (Ici 0) by
     simpa using this left_mem_Ici hx₀ hx₀
-  refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Ici _) (Continuous.continuousOn $ by
-    continuity) (fun x _ ↦
-    ((hasDerivAt_cos ..).add $ (hasDerivAt_pow ..).div_const _).hasDerivWithinAt) fun x hx ↦ ?_
-  simpa [mul_div_cancel_left] using sin_le $ interior_subset hx
+  refine monotoneOn_of_hasDerivWithinAt_nonneg
+    (convex_Ici _)
+    (Continuous.continuousOn <| by continuity)
+    (fun x _ ↦ ((hasDerivAt_cos ..).add <| (hasDerivAt_pow ..).div_const _).hasDerivWithinAt)
+    fun x hx ↦ ?_
+  simpa [mul_div_cancel_left] using sin_le <| interior_subset hx
 
 /-- **Jordan's inequality**. -/
 lemma two_div_pi_mul_le_sin (hx₀ : 0 ≤ x) (hx : x ≤ π / 2) : 2 / π * x ≤ sin x := by
@@ -98,8 +100,11 @@ lemma cos_quadratic_upper_bound (hx : |x| ≤ π) : cos x ≤ 1 - 2 / π ^ 2 * x
   simp only [Nat.cast_ofNat, Nat.succ_sub_succ_eq_sub, tsub_zero, pow_one, ← neg_sub', neg_sub,
     ← mul_assoc] at hderiv
   have hmono : MonotoneOn (fun x ↦ 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2)) := by
-    refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc ..) (Continuous.continuousOn $
-      by continuity) (fun x _ ↦ (hderiv _).hasDerivWithinAt) fun x hx ↦ sub_nonneg.2 ?_
+    refine monotoneOn_of_hasDerivWithinAt_nonneg
+      (convex_Icc ..)
+      (Continuous.continuousOn $ by continuity)
+      (fun x _ ↦ (hderiv _).hasDerivWithinAt)
+      fun x hx ↦ sub_nonneg.2 ?_
     have ⟨hx₀, hx⟩ := interior_subset hx
     calc 2 / π ^ 2 * 2 * x
         = 2 / π * (2 / π * x) := by ring
diff --git a/Mathlib/Combinatorics/SetFamily/Shadow.lean b/Mathlib/Combinatorics/SetFamily/Shadow.lean
index 15f9166f25050..a16e73cfae9c8 100644
--- a/Mathlib/Combinatorics/SetFamily/Shadow.lean
+++ b/Mathlib/Combinatorics/SetFamily/Shadow.lean
@@ -105,7 +105,7 @@ lemma mem_shadow_iff_exists_sdiff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s 
 
 /-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
 `𝒜`. -/
-lemma mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a, a ∉ t ∧ insert a t ∈ 𝒜 := by
+lemma mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜 := by
   simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
   aesop
 #align finset.mem_shadow_iff_insert_mem Finset.mem_shadow_iff_insert_mem
diff --git a/Mathlib/Data/Finset/Preimage.lean b/Mathlib/Data/Finset/Preimage.lean
index 8e8a66a5bab5e..b5895c608e95d 100644
--- a/Mathlib/Data/Finset/Preimage.lean
+++ b/Mathlib/Data/Finset/Preimage.lean
@@ -113,7 +113,7 @@ theorem preimage_subset {f : α ↪ β} {s : Finset β} {t : Finset α} (hs : s
 #align finset.preimage_subset Finset.preimage_subset
 
 theorem subset_map_iff {f : α ↪ β} {s : Finset β} {t : Finset α} :
-    s ⊆ t.map f ↔ ∃ u, u ⊆ t ∧ s = u.map f := by
+    s ⊆ t.map f ↔ ∃ u ⊆ t, s = u.map f := by
   classical
   simp_rw [← coe_subset, coe_map, subset_image_iff, map_eq_image, eq_comm]
 #align finset.subset_map_iff Finset.subset_map_iff
diff --git a/Mathlib/Data/Int/Order/Basic.lean b/Mathlib/Data/Int/Order/Basic.lean
index a08760fb3e5fd..fd92d0b5f331f 100644
--- a/Mathlib/Data/Int/Order/Basic.lean
+++ b/Mathlib/Data/Int/Order/Basic.lean
@@ -61,8 +61,8 @@ theorem abs_eq_natAbs : ∀ a : ℤ, |a| = natAbs a
 @[simp, norm_cast] lemma coe_natAbs (n : ℤ) : (n.natAbs : ℤ) = |n| := n.abs_eq_natAbs.symm
 #align int.coe_nat_abs Int.coe_natAbs
 
-lemma _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n| :=
-  by rw [← coe_natAbs, Int.cast_ofNat]
+lemma _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n| := by
+  rw [← coe_natAbs, Int.cast_ofNat]
 #align nat.cast_nat_abs Nat.cast_natAbs
 
 theorem natAbs_abs (a : ℤ) : natAbs |a| = natAbs a := by rw [abs_eq_natAbs]; rfl
diff --git a/Mathlib/Data/SetLike/Basic.lean b/Mathlib/Data/SetLike/Basic.lean
index 9142fef9dc209..72c06be28994e 100644
--- a/Mathlib/Data/SetLike/Basic.lean
+++ b/Mathlib/Data/SetLike/Basic.lean
@@ -187,7 +187,7 @@ theorem coe_eq_coe {x y : p} : (x : B) = y ↔ x = y :=
 #align set_like.coe_eq_coe SetLike.coe_eq_coe
 
 -- Porting note: this is not necessary anymore due to the way coercions work
- #noalign set_like.coe_mk
+#noalign set_like.coe_mk
 
 @[simp]
 theorem coe_mem (x : p) : (x : B) ∈ p :=
diff --git a/Mathlib/FieldTheory/PurelyInseparable.lean b/Mathlib/FieldTheory/PurelyInseparable.lean
index efe97fb36f4c2..68288b3e795b5 100644
--- a/Mathlib/FieldTheory/PurelyInseparable.lean
+++ b/Mathlib/FieldTheory/PurelyInseparable.lean
@@ -1005,8 +1005,8 @@ theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInsepara
     rintro x ⟨y, hy⟩
     obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y
     refine ⟨n, algebraMap F M z, ?_⟩
-    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow]
-    rfl
+    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
+      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
   have h := lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E L
     (IsPurelyInseparable.isAlgebraic F E)
   rw [IsPurelyInseparable.sepDegree_eq_one F E, Cardinal.lift_one, one_mul] at h
diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean
index 6a4f70e91307d..1e7f1e2635640 100644
--- a/Mathlib/GroupTheory/Perm/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Basic.lean
@@ -630,8 +630,8 @@ variable [AddGroup α] (a b : α)
 #align equiv.zpow_add_left Equiv.zpow_addLeft
 
 @[simp] lemma zpow_addRight : ∀ (n : ℤ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
-  | (Int.ofNat n) => by simp
-  | (Int.negSucc n) => by simp
+  | Int.ofNat n => by simp
+  | Int.negSucc n => by simp
 #align equiv.zpow_add_right Equiv.zpow_addRight
 
 end AddGroup
@@ -683,8 +683,8 @@ lemma zpow_mulLeft (n : ℤ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n) :=
 
 @[to_additive existing (attr := simp) zpow_addRight]
 lemma zpow_mulRight : ∀ n : ℤ, Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
-  | (Int.ofNat n) => by simp
-  | (Int.negSucc n) => by simp
+  | Int.ofNat n => by simp
+  | Int.negSucc n => by simp
 #align equiv.zpow_mul_right Equiv.zpow_mulRight
 
 end Group
@@ -709,8 +709,8 @@ lemma BijOn.perm_pow : BijOn f s s → ∀ n : ℕ, BijOn (f ^ n) s s := by
 #align set.bij_on.perm_pow Set.BijOn.perm_pow
 
 lemma BijOn.perm_zpow (hf : BijOn f s s) : ∀ n : ℤ, BijOn (f ^ n) s s
-  | (Int.ofNat n) => hf.perm_pow n
-  | (Int.negSucc n) => (hf.perm_pow (n + 1)).perm_inv
+  | Int.ofNat n => hf.perm_pow n
+  | Int.negSucc n => (hf.perm_pow (n + 1)).perm_inv
 #align set.bij_on.perm_zpow Set.BijOn.perm_zpow
 
 end Set
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 98e49642ceadb..20481c46af432 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -596,18 +596,18 @@ lemma forall_update_iff (f : ∀a, β a) {a : α} {b : β a} (p : ∀a, β a →
 #align function.forall_update_iff Function.forall_update_iff
 
 theorem exists_update_iff (f : ∀ a, β a) {a : α} {b : β a} (p : ∀ a, β a → Prop) :
-    (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ (x : _) (_ : x ≠ a), p x (f x) := by
+    (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x ≠ a, p x (f x) := by
   rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
   simp [-not_and, not_and_or]
 #align function.exists_update_iff Function.exists_update_iff
 
 theorem update_eq_iff {a : α} {b : β a} {f g : ∀ a, β a} :
-    update f a b = g ↔ b = g a ∧ ∀ (x) (_ : x ≠ a), f x = g x :=
+    update f a b = g ↔ b = g a ∧ ∀ x ≠ a, f x = g x :=
   funext_iff.trans <| forall_update_iff _ fun x y ↦ y = g x
 #align function.update_eq_iff Function.update_eq_iff
 
 theorem eq_update_iff {a : α} {b : β a} {f g : ∀ a, β a} :
-    g = update f a b ↔ g a = b ∧ ∀ (x) (_ : x ≠ a), g x = f x :=
+    g = update f a b ↔ g a = b ∧ ∀ x ≠ a, g x = f x :=
   funext_iff.trans <| forall_update_iff _ fun x y ↦ g x = y
 #align function.eq_update_iff Function.eq_update_iff
 
diff --git a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
index 72539080758ec..756a607b182ac 100644
--- a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
+++ b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
@@ -145,7 +145,7 @@ lemma hasSum_integral_of_summable_integral_norm {ι} [Countable ι] {F : ι →
   have (i : ι) : ∫⁻ (a : α), ‖F i a‖₊ ∂μ = ‖(∫ a : α, ‖F i a‖ ∂μ)‖₊ := by
     rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
       Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
-    rfl
+    simp only [coe_nnnorm]
   rw [funext this, ← ENNReal.coe_tsum]
   · apply coe_ne_top
   · simp_rw [← NNReal.summable_coe, coe_nnnorm]
diff --git a/Mathlib/MeasureTheory/Measure/NullMeasurable.lean b/Mathlib/MeasureTheory/Measure/NullMeasurable.lean
index 126c9dd9ad895..373158bf8e4ff 100644
--- a/Mathlib/MeasureTheory/Measure/NullMeasurable.lean
+++ b/Mathlib/MeasureTheory/Measure/NullMeasurable.lean
@@ -225,7 +225,7 @@ protected theorem insert [MeasurableSingletonClass (NullMeasurableSpace α μ)]
 #align measure_theory.null_measurable_set.insert MeasureTheory.NullMeasurableSet.insert
 
 theorem exists_measurable_superset_ae_eq (h : NullMeasurableSet s μ) :
-    ∃ t, t ⊇ s ∧ MeasurableSet t ∧ t =ᵐ[μ] s := by
+    ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s := by
   rcases h with ⟨t, htm, hst⟩
   refine' ⟨t ∪ toMeasurable μ (s \ t), _, htm.union (measurableSet_toMeasurable _ _), _⟩
   · exact diff_subset_iff.1 (subset_toMeasurable _ _)
@@ -243,7 +243,7 @@ theorem compl_toMeasurable_compl_ae_eq (h : NullMeasurableSet s μ) : (toMeasura
 #align measure_theory.null_measurable_set.compl_to_measurable_compl_ae_eq MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq
 
 theorem exists_measurable_subset_ae_eq (h : NullMeasurableSet s μ) :
-    ∃ t, t ⊆ s ∧ MeasurableSet t ∧ t =ᵐ[μ] s :=
+    ∃ t ⊆ s, MeasurableSet t ∧ t =ᵐ[μ] s :=
   ⟨(toMeasurable μ sᶜ)ᶜ, compl_subset_comm.2 <| subset_toMeasurable _ _,
     (measurableSet_toMeasurable _ _).compl, compl_toMeasurable_compl_ae_eq h⟩
 #align measure_theory.null_measurable_set.exists_measurable_subset_ae_eq MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
diff --git a/Mathlib/MeasureTheory/Measure/Regular.lean b/Mathlib/MeasureTheory/Measure/Regular.lean
index 6a5595890ea6d..7f8441860b5c8 100644
--- a/Mathlib/MeasureTheory/Measure/Regular.lean
+++ b/Mathlib/MeasureTheory/Measure/Regular.lean
@@ -418,7 +418,7 @@ lemma of_restrict [OpensMeasurableSpace α] {μ : Measure α} {s : ℕ → Set 
     rw [← inter_iUnion, iUnion_disjointed, univ_subset_iff.mp h'', inter_univ]
   rcases ENNReal.exists_pos_sum_of_countable' (tsub_pos_iff_lt.2 hr).ne' ℕ with ⟨δ, δ0, hδε⟩
   rw [lt_tsub_iff_right, add_comm] at hδε
-  have : ∀ n, ∃ (U : _) (_ : U ⊇ A n), IsOpen U ∧ μ U < μ (A n) + δ n := by
+  have : ∀ n, ∃ U ⊇ A n, IsOpen U ∧ μ U < μ (A n) + δ n := by
     intro n
     have H₁ : ∀ t, μ.restrict (s n) t = μ (t ∩ s n) := fun t => restrict_apply' (hm n)
     have Ht : μ.restrict (s n) (A n) ≠ ∞ := by
@@ -470,7 +470,7 @@ theorem measurableSet_of_isOpen [OuterRegular μ] (H : InnerRegularWRT μ p IsOp
     have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
     obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
     simpa using hd hK isOpen_univ
-  obtain ⟨ε, hε, hεs, rfl⟩ : ∃ (ε : _) (_ : ε ≠ 0), ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
+  obtain ⟨ε, hε, hεs, rfl⟩ : ∃ ε ≠ 0, ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
     use (μ s - r) / 2
     simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, le_add_right, tsub_eq_zero_iff_le]
   rcases hs.exists_isOpen_diff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩
diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean
index 89111cf1d000a..4f1a654f92b3e 100644
--- a/Mathlib/MeasureTheory/Measure/Typeclasses.lean
+++ b/Mathlib/MeasureTheory/Measure/Typeclasses.lean
@@ -1425,7 +1425,7 @@ variable [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s : Set 
 /-- If `s` is a compact set and `μ` is finite at `𝓝 x` for every `x ∈ s`, then `s` admits an open
 superset of finite measure. -/
 theorem exists_open_superset_measure_lt_top' (h : IsCompact s)
-    (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)) : ∃ (U : _) (_ : U ⊇ s), IsOpen U ∧ μ U < ∞ := by
+    (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)) : ∃ U ⊇ s, IsOpen U ∧ μ U < ∞ := by
   refine' IsCompact.induction_on h _ _ _ _
   · use ∅
     simp [Superset]
@@ -1443,7 +1443,7 @@ theorem exists_open_superset_measure_lt_top' (h : IsCompact s)
 /-- If `s` is a compact set and `μ` is a locally finite measure, then `s` admits an open superset of
 finite measure. -/
 theorem exists_open_superset_measure_lt_top (h : IsCompact s) (μ : Measure α)
-    [IsLocallyFiniteMeasure μ] : ∃ (U : _) (_ : U ⊇ s), IsOpen U ∧ μ U < ∞ :=
+    [IsLocallyFiniteMeasure μ] : ∃ U ⊇ s, IsOpen U ∧ μ U < ∞ :=
   h.exists_open_superset_measure_lt_top' fun x _ => μ.finiteAt_nhds x
 #align is_compact.exists_open_superset_measure_lt_top IsCompact.exists_open_superset_measure_lt_top
 
@@ -1493,13 +1493,13 @@ def MeasureTheory.Measure.finiteSpanningSetsInOpen [TopologicalSpace α] [SigmaC
     μ.FiniteSpanningSetsIn { K | IsOpen K } where
   set n := ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose
   set_mem n :=
-    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.snd.1
+    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.2.1
   finite n :=
-    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.snd.2
+    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.2.2
   spanning :=
     eq_univ_of_subset
       (iUnion_mono fun n =>
-        ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.fst)
+        ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.1)
       (iUnion_compactCovering α)
 #align measure_theory.measure.finite_spanning_sets_in_open MeasureTheory.Measure.finiteSpanningSetsInOpen
 
diff --git a/Mathlib/MeasureTheory/OuterMeasure/Basic.lean b/Mathlib/MeasureTheory/OuterMeasure/Basic.lean
index 3413680f7791c..31c32ae43e638 100644
--- a/Mathlib/MeasureTheory/OuterMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/OuterMeasure/Basic.lean
@@ -1484,8 +1484,8 @@ theorem inducedOuterMeasure_preimage (f : α ≃ α) (Pm : ∀ s : Set α, P (f
 
 theorem inducedOuterMeasure_exists_set {s : Set α} (hs : inducedOuterMeasure m P0 m0 s ≠ ∞)
     {ε : ℝ≥0∞} (hε : ε ≠ 0) :
-    ∃ (t : Set α) (_ht : P t),
-      s ⊆ t ∧ inducedOuterMeasure m P0 m0 t ≤ inducedOuterMeasure m P0 m0 s + ε := by
+    ∃ t : Set α,
+      P t ∧ s ⊆ t ∧ inducedOuterMeasure m P0 m0 t ≤ inducedOuterMeasure m P0 m0 s + ε := by
   have h := ENNReal.lt_add_right hs hε
   conv at h =>
     lhs
diff --git a/Mathlib/NumberTheory/Harmonic/Defs.lean b/Mathlib/NumberTheory/Harmonic/Defs.lean
index 2bb005937373a..1b40de4f80caa 100644
--- a/Mathlib/NumberTheory/Harmonic/Defs.lean
+++ b/Mathlib/NumberTheory/Harmonic/Defs.lean
@@ -31,10 +31,11 @@ lemma harmonic_zero : harmonic 0 = 0 :=
 lemma harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹ :=
   Finset.sum_range_succ ..
 
-lemma harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n :=
-  Finset.sum_pos (fun _ _ => inv_pos.mpr (by norm_cast; linarith)) <|
-    Finset.nonempty_range_iff.mpr Hn
+lemma harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n := by
+  unfold harmonic
+  rw [← Finset.nonempty_range_iff] at Hn
+  positivity
 
-lemma harmonic_eq_sum_Icc {n : ℕ} :  harmonic n = ∑ i in Finset.Icc 1 n, (↑i)⁻¹ := by
+lemma harmonic_eq_sum_Icc {n : ℕ} : harmonic n = ∑ i in Finset.Icc 1 n, (↑i)⁻¹ := by
   rw [harmonic, Finset.range_eq_Ico, Finset.sum_Ico_add' (fun (i : ℕ) ↦ (i : ℚ)⁻¹) 0 n (c := 1),
     Nat.Ico_succ_right]
diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean
index b75ba81ba33d1..6bb13e647b88b 100644
--- a/Mathlib/NumberTheory/NumberField/Embeddings.lean
+++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean
@@ -277,9 +277,9 @@ namespace NumberField.InfinitePlace
 
 open NumberField
 
-instance {K : Type*} [Field K] : FunLike (InfinitePlace K) K ℝ :=
-{ coe := fun w x => w.1 x
-  coe_injective' := fun _ _ h => Subtype.eq (AbsoluteValue.ext fun x => congr_fun h x)}
+instance {K : Type*} [Field K] : FunLike (InfinitePlace K) K ℝ where
+  coe w x := w.1 x
+  coe_injective' := fun _ _ h => Subtype.eq (AbsoluteValue.ext fun x => congr_fun h x)
 
 instance : MonoidWithZeroHomClass (InfinitePlace K) K ℝ where
   map_mul w _ _ := w.1.map_mul _ _
@@ -1057,12 +1057,12 @@ theorem nrRealPlaces_eq_zero_of_two_lt (hk : 2 < k) (hζ : IsPrimitiveRoot ζ k)
   let f := w.embedding
   have hζ' : IsPrimitiveRoot (f ζ) k := hζ.map_of_injective f.injective
   have him : (f ζ).im = 0 := by
-    · rw [← Complex.conj_eq_iff_im, ← NumberField.ComplexEmbedding.conjugate_coe_eq]
-      congr
+    rw [← Complex.conj_eq_iff_im, ← NumberField.ComplexEmbedding.conjugate_coe_eq]
+    congr
   have hre : (f ζ).re = 1 ∨ (f ζ).re = -1 := by
-    · rw [← Complex.abs_re_eq_abs] at him
-      have := Complex.norm_eq_one_of_pow_eq_one hζ'.pow_eq_one (by linarith)
-      rwa [Complex.norm_eq_abs, ← him, ← abs_one, abs_eq_abs] at this
+    rw [← Complex.abs_re_eq_abs] at him
+    have := Complex.norm_eq_one_of_pow_eq_one hζ'.pow_eq_one (by linarith)
+    rwa [Complex.norm_eq_abs, ← him, ← abs_one, abs_eq_abs] at this
   cases hre with
   | inl hone =>
     exact hζ'.ne_one (by linarith) <| Complex.ext (by simp [hone]) (by simp [him])
diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
index 4107f9f2033f3..2cad7f6519337 100644
--- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean
+++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -966,7 +966,7 @@ variable {p : ℕ} [hp : Fact p.Prime]
 -- Porting note: remove `set_option eqn_compiler.zeta true`
 
 instance complete : CauSeq.IsComplete ℚ_[p] norm where
-  isComplete := fun f => by
+  isComplete f := by
     have cau_seq_norm_e : IsCauSeq padicNormE f := fun ε hε => by
       have h := isCauSeq f ε (mod_cast hε)
       dsimp [norm] at h
diff --git a/Mathlib/Order/Partition/Finpartition.lean b/Mathlib/Order/Partition/Finpartition.lean
index fb04149e86946..3b4440b1f8d33 100644
--- a/Mathlib/Order/Partition/Finpartition.lean
+++ b/Mathlib/Order/Partition/Finpartition.lean
@@ -557,12 +557,9 @@ def atomise (s : Finset α) (F : Finset (Finset α)) : Finpartition s :=
 
 variable {F : Finset (Finset α)}
 
--- Porting note:
-/- ./././Mathport/Syntax/Translate/Basic.lean:632:2: warning: expanding binder collection
-   (Q «expr ⊆ » F) -/
 theorem mem_atomise :
     t ∈ (atomise s F).parts ↔
-      t.Nonempty ∧ ∃ (Q : _) (_ : Q ⊆ F), (s.filter fun i ↦ ∀ u ∈ F, u ∈ Q ↔ i ∈ u) = t := by
+      t.Nonempty ∧ ∃ Q ⊆ F, (s.filter fun i ↦ ∀ u ∈ F, u ∈ Q ↔ i ∈ u) = t := by
   simp only [atomise, ofErase, bot_eq_empty, mem_erase, mem_image, nonempty_iff_ne_empty,
     mem_singleton, and_comm, mem_powerset, exists_prop]
 #align finpartition.mem_atomise Finpartition.mem_atomise
@@ -597,7 +594,7 @@ theorem card_filter_atomise_le_two_pow (ht : t ∈ F) :
     rw [card_powerset, card_erase_of_mem ht]
   rw [subset_iff]
   simp_rw [mem_image, mem_powerset, mem_filter, and_imp, Finset.Nonempty, exists_imp, mem_atomise,
-    and_imp, Finset.Nonempty, exists_imp]
+    and_imp, Finset.Nonempty, exists_imp, and_imp]
   rintro P' i hi P PQ rfl hy₂ j _hj
   refine' ⟨P.erase t, erase_subset_erase _ PQ, _⟩
   simp only [insert_erase (((mem_filter.1 hi).2 _ ht).2 <| hy₂ hi)]
diff --git a/Mathlib/Order/SupIndep.lean b/Mathlib/Order/SupIndep.lean
index 4d0996eb92052..8163fdf28025c 100644
--- a/Mathlib/Order/SupIndep.lean
+++ b/Mathlib/Order/SupIndep.lean
@@ -361,7 +361,7 @@ theorem independent_def' : Independent t ↔ ∀ i, Disjoint (t i) (sSup (t '' {
 #align complete_lattice.independent_def' CompleteLattice.independent_def'
 
 theorem independent_def'' :
-    Independent t ↔ ∀ i, Disjoint (t i) (sSup { a | ∃ (j : _) (_ : j ≠ i), t j = a }) := by
+    Independent t ↔ ∀ i, Disjoint (t i) (sSup { a | ∃ j ≠ i, t j = a }) := by
   rw [independent_def']
   aesop
 #align complete_lattice.independent_def'' CompleteLattice.independent_def''
diff --git a/Mathlib/Order/ZornAtoms.lean b/Mathlib/Order/ZornAtoms.lean
index 890537681c157..44ddc612105a1 100644
--- a/Mathlib/Order/ZornAtoms.lean
+++ b/Mathlib/Order/ZornAtoms.lean
@@ -24,7 +24,7 @@ bound not equal to `⊤`. -/
 theorem IsCoatomic.of_isChain_bounded {α : Type*} [PartialOrder α] [OrderTop α]
     (h :
       ∀ c : Set α,
-        IsChain (· ≤ ·) c → c.Nonempty → ⊤ ∉ c → ∃ (x : _) (_ : x ≠ ⊤), x ∈ upperBounds c) :
+        IsChain (· ≤ ·) c → c.Nonempty → ⊤ ∉ c → ∃ x ≠ ⊤, x ∈ upperBounds c) :
     IsCoatomic α := by
   refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
   have : ∃ y ∈ Ico x ⊤, x ≤ y ∧ ∀ z ∈ Ico x ⊤, y ≤ z → z = y := by
@@ -41,7 +41,7 @@ bound not equal to `⊥`. -/
 theorem IsAtomic.of_isChain_bounded {α : Type*} [PartialOrder α] [OrderBot α]
     (h :
       ∀ c : Set α,
-        IsChain (· ≤ ·) c → c.Nonempty → ⊥ ∉ c → ∃ (x : _) (_ : x ≠ ⊥), x ∈ lowerBounds c) :
+        IsChain (· ≤ ·) c → c.Nonempty → ⊥ ∉ c → ∃ x ≠ ⊥, x ∈ lowerBounds c) :
     IsAtomic α :=
   isCoatomic_dual_iff_isAtomic.mp <| IsCoatomic.of_isChain_bounded fun c hc => h c hc.symm
 #align is_atomic.of_is_chain_bounded IsAtomic.of_isChain_bounded
diff --git a/Mathlib/RingTheory/Algebraic.lean b/Mathlib/RingTheory/Algebraic.lean
index 360c18b3536d7..92b5ceb14feca 100644
--- a/Mathlib/RingTheory/Algebraic.lean
+++ b/Mathlib/RingTheory/Algebraic.lean
@@ -389,7 +389,7 @@ variable {R S : Type*} [CommRing R] [IsDomain R] [CommRing S]
 
 theorem exists_integral_multiple [Algebra R S] {z : S} (hz : IsAlgebraic R z)
     (inj : ∀ x, algebraMap R S x = 0 → x = 0) :
-    ∃ (x : integralClosure R S) (y : _) (_ : y ≠ (0 : R)), z * algebraMap R S y = x := by
+    ∃ᵉ (x : integralClosure R S) (y ≠ (0 : R)), z * algebraMap R S y = x := by
   rcases hz with ⟨p, p_ne_zero, px⟩
   set a := p.leadingCoeff
   have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero
@@ -404,7 +404,7 @@ if `S` is the integral closure of `R` in an algebraic extension `L` of `R`. -/
 theorem IsIntegralClosure.exists_smul_eq_mul {L : Type*} [Field L] [Algebra R S] [Algebra S L]
     [Algebra R L] [IsScalarTower R S L] [IsIntegralClosure S R L] (h : Algebra.IsAlgebraic R L)
     (inj : Function.Injective (algebraMap R L)) (a : S) {b : S} (hb : b ≠ 0) :
-    ∃ (c : S) (d : _) (_ : d ≠ (0 : R)), d • a = b * c := by
+    ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c := by
   obtain ⟨c, d, d_ne, hx⟩ :=
     exists_integral_multiple (h (algebraMap _ L a / algebraMap _ L b))
       ((injective_iff_map_eq_zero _).mp inj)
diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean
index ff999268bb9ae..98e39469e195e 100644
--- a/Mathlib/RingTheory/Ideal/Basic.lean
+++ b/Mathlib/RingTheory/Ideal/Basic.lean
@@ -234,7 +234,7 @@ theorem mem_span_singleton_sup {S : Type*} [CommSemiring S] {x y : S} {I : Ideal
 /-- The ideal generated by an arbitrary binary relation.
 -/
 def ofRel (r : α → α → Prop) : Ideal α :=
-  Submodule.span α { x | ∃ (a b : _) (_h : r a b), x + b = a }
+  Submodule.span α { x | ∃ a b, r a b ∧ x + b = a }
 #align ideal.of_rel Ideal.ofRel
 
 /-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/
diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean
index 4b549848d8dd1..00b210ccfa751 100644
--- a/Mathlib/RingTheory/Polynomial/Basic.lean
+++ b/Mathlib/RingTheory/Polynomial/Basic.lean
@@ -197,7 +197,7 @@ theorem exists_degree_le_of_mem_span {s : Set R[X]} {p : R[X]}
   by_contra! h
   by_cases hp_zero : p = 0
   · rw [hp_zero, degree_zero] at h
-    rcases hs with ⟨x,hx⟩
+    rcases hs with ⟨x, hx⟩
     exact not_lt_bot (h x hx)
   · have : p ∈ degreeLT R (natDegree p) := by
       refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp
@@ -214,9 +214,8 @@ theorem exists_degree_le_of_mem_span_of_finite {s : Set R[X]} (s_fin : s.Finite)
   rcases Set.Finite.exists_maximal_wrt degree s s_fin hs with ⟨a, has, hmax⟩
   refine ⟨a, has, fun p hp => ?_⟩
   rcases exists_degree_le_of_mem_span hs hp with ⟨p', hp'⟩
-  have p'max := hmax p' hp'.left
   by_cases h : degree a ≤ degree p'
-  · rw [← p'max h] at hp'; exact hp'.right
+  · rw [← hmax p' hp'.left h] at hp'; exact hp'.right
   · exact le_trans hp'.right (not_le.mp h).le
 
 /-- The span of every finite set of polynomials is contained in a `degreeLE n` for some `n`. -/
diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean
index 59ea99475a7d7..d44cd5e264539 100644
--- a/Mathlib/SetTheory/Ordinal/Principal.lean
+++ b/Mathlib/SetTheory/Ordinal/Principal.lean
@@ -149,7 +149,7 @@ theorem principal_add_iff_add_left_eq_self {o : Ordinal} :
 #align ordinal.principal_add_iff_add_left_eq_self Ordinal.principal_add_iff_add_left_eq_self
 
 theorem exists_lt_add_of_not_principal_add {a} (ha : ¬Principal (· + ·) a) :
-    ∃ (b c : _) (_ : b < a) (_ : c < a), b + c = a := by
+    ∃ b c, b < a ∧ c < a ∧ b + c = a := by
   unfold Principal at ha
   push_neg at ha
   rcases ha with ⟨b, c, hb, hc, H⟩
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index aff9ccdbb45ad..e122178b52570 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -63,8 +63,7 @@ theorem summable_iff_of_summable_sub (hfg : Summable fun b ↦ f b - g b) :
 
 theorem HasSum.update (hf : HasSum f a₁) (b : β) [DecidableEq β] (a : α) :
     HasSum (update f b a) (a - f b + a₁) := by
-  convert (hasSum_ite_eq b (a - f b)).add hf
-  rename_i b'
+  convert (hasSum_ite_eq b (a - f b)).add hf with b'
   by_cases h : b' = b
   · rw [h, update_same]
     simp [eq_self_iff_true, if_true, sub_add_cancel]
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
index 257e6b94c2202..a679682776863 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
@@ -190,8 +190,7 @@ variable [TopologicalSpace G] [TopologicalAddGroup G]
 theorem hasSum_nat_add_iff {f : ℕ → G} (k : ℕ) :
     HasSum (fun n ↦ f (n + k)) g ↔ HasSum f (g + ∑ i in range k, f i) := by
   refine Iff.trans ?_ (range k).hasSum_compl_iff
-  rw [← (notMemRangeEquiv k).symm.hasSum_iff]
-  rfl
+  rw [← (notMemRangeEquiv k).symm.hasSum_iff, Function.comp_def, coe_notMemRangeEquiv_symm]
 #align has_sum_nat_add_iff hasSum_nat_add_iff
 
 theorem summable_nat_add_iff {f : ℕ → G} (k : ℕ) : (Summable fun n ↦ f (n + k)) ↔ Summable f :=
diff --git a/Mathlib/Topology/Algebra/Module/LinearPMap.lean b/Mathlib/Topology/Algebra/Module/LinearPMap.lean
index 2716e4e4a333c..221507d2a3011 100644
--- a/Mathlib/Topology/Algebra/Module/LinearPMap.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearPMap.lean
@@ -144,7 +144,7 @@ theorem IsClosable.closureIsClosable {f : E →ₗ.[R] F} (hf : f.IsClosable) :
 #align linear_pmap.is_closable.closure_is_closable LinearPMap.IsClosable.closureIsClosable
 
 theorem isClosable_iff_exists_closed_extension {f : E →ₗ.[R] F} :
-    f.IsClosable ↔ ∃ (g : E →ₗ.[R] F) (_ : g.IsClosed), f ≤ g :=
+    f.IsClosable ↔ ∃ g : E →ₗ.[R] F, g.IsClosed ∧ f ≤ g :=
   ⟨fun h => ⟨f.closure, h.closure_isClosed, f.le_closure⟩, fun ⟨_, hg, h⟩ =>
     hg.isClosable.leIsClosable h⟩
 #align linear_pmap.is_closable_iff_exists_closed_extension LinearPMap.isClosable_iff_exists_closed_extension
diff --git a/Mathlib/Topology/Baire/CompleteMetrizable.lean b/Mathlib/Topology/Baire/CompleteMetrizable.lean
index 68e6b609c94ec..cd812ad58ccf0 100644
--- a/Mathlib/Topology/Baire/CompleteMetrizable.lean
+++ b/Mathlib/Topology/Baire/CompleteMetrizable.lean
@@ -71,15 +71,15 @@ instance (priority := 100) BaireSpace.of_pseudoEMetricSpace_completeSpace : Bair
   let r : ℕ → ℝ≥0∞ := fun n => (F n).2
   have rpos : ∀ n, 0 < r n := by
     intro n
-    induction' n with n hn
-    exact lt_min εpos (Bpos 0)
-    exact Hpos n (c n) (r n) hn.ne'
+    induction n with
+    | zero => exact lt_min εpos (Bpos 0)
+    | succ n hn => exact Hpos n (c n) (r n) hn.ne'
   have r0 : ∀ n, r n ≠ 0 := fun n => (rpos n).ne'
   have rB : ∀ n, r n ≤ B n := by
     intro n
-    induction' n with n _
-    exact min_le_right _ _
-    exact HB n (c n) (r n) (r0 n)
+    cases n with
+    | zero => exact min_le_right _ _
+    | succ n => exact HB n (c n) (r n) (r0 n)
   have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n :=
     fun n => Hball n (c n) (r n) (r0 n)
   have cdist : ∀ n, edist (c n) (c (n + 1)) ≤ B n := by
@@ -118,4 +118,3 @@ instance (priority := 100) BaireSpace.of_pseudoEMetricSpace_completeSpace : Bair
   show edist y x ≤ ε
   exact le_trans (yball 0) (min_le_left _ _)
 #align baire_category_theorem_emetric_complete BaireSpace.of_pseudoEMetricSpace_completeSpace
-
diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean
index e50dc8aaa4a26..c019e31199bbf 100644
--- a/Mathlib/Topology/Constructions.lean
+++ b/Mathlib/Topology/Constructions.lean
@@ -1534,12 +1534,9 @@ theorem pi_generateFrom_eq_finite {π : ι → Type*} {g : ∀ a, Set (Set (π a
     by_cases a ∈ i <;> simp [*]
 #align pi_generate_from_eq_finite pi_generateFrom_eq_finite
 
--- Porting note (#10756): new lemma
 theorem induced_to_pi {X : Type*} (f : X → ∀ i, π i) :
     induced f Pi.topologicalSpace = ⨅ i, induced (f · i) inferInstance := by
-  erw [induced_iInf]
-  simp only [induced_compose]
-  rfl
+  simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp]
 
 /-- Suppose `π i` is a family of topological spaces indexed by `i : ι`, and `X` is a type
 endowed with a family of maps `f i : X → π i` for every `i : ι`, hence inducing a
@@ -1721,9 +1718,7 @@ section ULift
 
 theorem ULift.isOpen_iff [TopologicalSpace X] {s : Set (ULift.{v} X)} :
     IsOpen s ↔ IsOpen (ULift.up ⁻¹' s) := by
-  unfold ULift.topologicalSpace
-  erw [← Equiv.ulift.coinduced_symm]
-  rfl
+  rw [ULift.topologicalSpace, ← Equiv.ulift_apply, ← Equiv.ulift.coinduced_symm, ← isOpen_coinduced]
 
 theorem ULift.isClosed_iff [TopologicalSpace X] {s : Set (ULift.{v} X)} :
     IsClosed s ↔ IsClosed (ULift.up ⁻¹' s) := by
diff --git a/Mathlib/Topology/MetricSpace/Closeds.lean b/Mathlib/Topology/MetricSpace/Closeds.lean
index 383e04c10d612..2e73f479954aa 100644
--- a/Mathlib/Topology/MetricSpace/Closeds.lean
+++ b/Mathlib/Topology/MetricSpace/Closeds.lean
@@ -203,7 +203,7 @@ instance Closeds.compactSpace [CompactSpace α] : CompactSpace (Closeds α) :=
       EMetric.totallyBounded_iff.1
         (isCompact_iff_totallyBounded_isComplete.1 (@isCompact_univ α _ _)).1 δ δpos
     -- we first show that any set is well approximated by a subset of `s`.
-    have main : ∀ u : Set α, ∃ (v : _) (_ : v ⊆ s), hausdorffEdist u v ≤ δ := by
+    have main : ∀ u : Set α, ∃ v ⊆ s, hausdorffEdist u v ≤ δ := by
       intro u
       let v := { x : α | x ∈ s ∧ ∃ y ∈ u, edist x y < δ }
       exists v, (fun x hx => hx.1 : v ⊆ s)