chore: tidy various files

Ruben-VandeVelde · Ruben-VandeVelde · commit 05fc0b6ed4db · 2025-02-03T19:15:48.000+01:00
diff --git a/Mathlib/Algebra/Lie/Engel.lean b/Mathlib/Algebra/Lie/Engel.lean
@@ -243,9 +243,7 @@ theorem LieAlgebra.isEngelian_of_isNoetherian [IsNoetherian R L] : LieAlgebra.Is
           K.toSubmodule_inj]
       exact Submodule.Quotient.nontrivial_of_lt_top _ hK₂.lt_top
     have : LieModule.IsNilpotent K (L' ⧸ K.toLieSubmodule) := by
-      -- Porting note: was refine' hK₁ _ fun x => _
-      apply hK₁
-      intro x
+      refine hK₁ _ fun x => ?_
       have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
       apply Module.End.IsNilpotent.mapQ ?_ hx
       -- Porting note: mathlib3 solved this on its own with `submodule.mapq_linear._proof_5`
diff --git a/Mathlib/Algebra/Lie/Nilpotent.lean b/Mathlib/Algebra/Lie/Nilpotent.lean
@@ -105,8 +105,7 @@ private theorem coe_lowerCentralSeries_eq_int_aux (R₁ R₂ L M : Type*)
 
 theorem coe_lowerCentralSeries_eq_int [LieModule R L M] (k : ℕ) :
     (lowerCentralSeries R L M k : Set M) = (lowerCentralSeries ℤ L M k : Set M) := by
-  show ((lowerCentralSeries R L M k).toSubmodule : Set M) =
-       ((lowerCentralSeries ℤ L M k).toSubmodule : Set M)
+  rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule]
   induction k with
   | zero => rfl
   | succ k ih =>
diff --git a/Mathlib/Algebra/Lie/Solvable.lean b/Mathlib/Algebra/Lie/Solvable.lean
@@ -226,8 +226,8 @@ private theorem coe_derivedSeries_eq_int_aux (R₁ R₂ L : Type*) [CommRing R
 
 theorem coe_derivedSeries_eq_int (k : ℕ) :
     (derivedSeries R L k : Set L) = (derivedSeries ℤ L k : Set L) := by
-  show ((derivedSeries R L k).toSubmodule : Set L) = ((derivedSeries ℤ L k).toSubmodule : Set L)
-  rw [derivedSeries_def, derivedSeries_def]
+  rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule, derivedSeries_def,
+    derivedSeries_def]
   induction k with
   | zero => rfl
   | succ k ih =>
diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean
@@ -1009,8 +1009,7 @@ theorem sub_floor_div_mul_nonneg (a : k) (hb : 0 < b) : 0 ≤ a - ⌊a / b⌋ *
 
 theorem sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b :=
   sub_lt_iff_lt_add.2 <| by
-    -- Porting note: `← one_add_mul` worked in mathlib3 without the argument
-    rw [← one_add_mul _ b, ← div_lt_iff₀ hb, add_comm]
+    rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]
     exact lt_floor_add_one _
 
 theorem fract_div_natCast_eq_div_natCast_mod {m n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n := by
@@ -1055,7 +1054,7 @@ theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} :
     -- Porting note: the `simp` was `push_cast`
     simp [m₁]
   · congr 2
-    change (q * ↑n - (↑m₀ : ℤ)) % ↑n = _
+    simp only [m₁]
     rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self]
 
 end LinearOrderedField
diff --git a/Mathlib/Algebra/Order/Round.lean b/Mathlib/Algebra/Order/Round.lean
@@ -205,10 +205,6 @@ variable [LinearOrderedField α] [LinearOrderedField β] [FloorRing α] [FloorRi
 variable [FunLike F α β] [RingHomClass F α β] {a : α} {b : β}
 
 theorem map_round (f : F) (hf : StrictMono f) (a : α) : round (f a) = round a := by
-  have H : f 2 = 2 := map_natCast f 2
-  simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, H]
-  -- Porting note: was
-  -- simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_bit0, map_one]
-  -- Would have thought that `map_natCast` would replace `map_bit0, map_one` but seems not
+  simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]
 
 end Int
diff --git a/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean b/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
@@ -116,17 +116,17 @@ theorem natDegree_mul_C_eq_of_mul_eq_one {ai : R} (au : a * ai = 1) :
       _ = (p * C a * C ai).natDegree := by rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
       _ ≤ (p * C a).natDegree := natDegree_mul_C_le (p * C a) ai)
 
-/-- Although not explicitly stated, the assumptions of lemma `nat_degree_mul_C_eq_of_mul_ne_zero`
-force the polynomial `p` to be non-zero, via `p.leading_coeff ≠ 0`.
+/-- Although not explicitly stated, the assumptions of lemma `natDegree_mul_C_eq_of_mul_ne_zero`
+force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
 -/
 theorem natDegree_mul_C_eq_of_mul_ne_zero (h : p.leadingCoeff * a ≠ 0) :
     (p * C a).natDegree = p.natDegree := by
   refine eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_
   refine mem_support_iff.mpr ?_
   rwa [coeff_mul_C]
 
-/-- Although not explicitly stated, the assumptions of lemma `nat_degree_C_mul_eq_of_mul_ne_zero`
-force the polynomial `p` to be non-zero, via `p.leading_coeff ≠ 0`.
+/-- Although not explicitly stated, the assumptions of lemma `natDegree_C_mul_of_mul_ne_zero`
+force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
 -/
 theorem natDegree_C_mul_of_mul_ne_zero (h : a * p.leadingCoeff ≠ 0) :
     (C a * p).natDegree = p.natDegree := by
diff --git a/Mathlib/Algebra/Polynomial/Degree/Operations.lean b/Mathlib/Algebra/Polynomial/Degree/Operations.lean
@@ -12,7 +12,7 @@ import Mathlib.Algebra.Polynomial.Degree.Definitions
 ## Main results
 - `degree_mul` : The degree of the product is the sum of degrees
 - `leadingCoeff_add_of_degree_eq` and `leadingCoeff_add_of_degree_lt` :
-    The leading_coefficient of a sum is determined by the leading coefficients and degrees
+    The leading coefficient of a sum is determined by the leading coefficients and degrees
 -/
 
 noncomputable section
diff --git a/Mathlib/Algebra/Polynomial/Laurent.lean b/Mathlib/Algebra/Polynomial/Laurent.lean
@@ -66,7 +66,7 @@ Lots is missing!
 --  This would likely involve adding a `comapDomain` analogue of
 --  `AddMonoidAlgebra.mapDomainAlgHom` and an `R`-linear version of
 --  `Polynomial.toFinsuppIso`.
--- Add `degree, int_degree, int_trailing_degree, leading_coeff, trailing_coeff,...`.
+-- Add `degree, intDegree, intTrailingDegree, leadingCoeff, trailingCoeff,...`.
 -/
 
 
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
@@ -676,9 +676,9 @@ lemma of_stalkMap (hQ : OfLocalizationPrime Q) (H : ∀ x, Q (f.stalkMap x).hom)
 /-- Let `Q` be a property of ring maps that is stable under localization.
 Then if the associated property of scheme morphisms holds for `f`, `Q` holds on all stalks. -/
 lemma stalkMap
-      (hQ : ∀ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (_ : Q f)
-        (J : Ideal S) (_ : J.IsPrime), Q (Localization.localRingHom _ J f rfl))
-      (hf : P f) (x : X) : Q (f.stalkMap x).hom := by
+    (hQ : ∀ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (_ : Q f)
+      (J : Ideal S) (_ : J.IsPrime), Q (Localization.localRingHom _ J f rfl))
+    (hf : P f) (x : X) : Q (f.stalkMap x).hom := by
   have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
   wlog h : IsAffine X ∧ IsAffine Y generalizing X Y f
   · obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open Y)
diff --git a/Mathlib/Analysis/Calculus/Deriv/Prod.lean b/Mathlib/Analysis/Calculus/Deriv/Prod.lean
@@ -82,8 +82,7 @@ theorem derivWithin_pi (h : ∀ i, DifferentiableWithinAt 𝕜 (fun x => φ x i)
     derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x := by
   rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs
   · exact (hasDerivWithinAt_pi.2 fun i => (h i).hasDerivWithinAt).derivWithin hxs
-  · simp only [derivWithin_zero_of_isolated hxs]
-    rfl
+  · simp only [derivWithin_zero_of_isolated hxs, Pi.zero_def]
 
 theorem deriv_pi (h : ∀ i, DifferentiableAt 𝕜 (fun x => φ x i) x) :
     deriv φ x = fun i => deriv (fun x => φ x i) x :=
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean b/Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
@@ -9,7 +9,7 @@ import Mathlib.Analysis.Calculus.FDeriv.Prod
 # The derivative of bounded bilinear maps
 
 For detailed documentation of the Fréchet derivative,
-see the module docstring of `Analysis/Calculus/FDeriv/Basic.lean`.
+see the module docstring of `Mathlib/Analysis/Calculus/FDeriv/Basic.lean`.
 
 This file contains the usual formulas (and existence assertions) for the derivative of
 bounded bilinear maps.
diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
@@ -105,7 +105,7 @@ theorem iteratedDerivWithin_zero : iteratedDerivWithin 0 f s = f := by
 theorem iteratedDerivWithin_one {x : 𝕜} :
     iteratedDerivWithin 1 f s x = derivWithin f s x := by
   rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs
-  · simp only [iteratedDerivWithin, iteratedFDerivWithin_one_apply hxs]; rfl
+  · simp only [iteratedDerivWithin, iteratedFDerivWithin_one_apply hxs, derivWithin]
   · simp [derivWithin_zero_of_isolated hxs, iteratedDerivWithin, iteratedFDerivWithin,
       fderivWithin_zero_of_isolated hxs]
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals.lean b/Mathlib/Analysis/SpecialFunctions/Integrals.lean
@@ -498,14 +498,14 @@ lemma integral_log_from_zero_of_pos (ht : 0 < b) : ∫ s in (0)..b, log s = b *
 
 /-- Helper lemma for `integral_log`: case where `a = 0`. -/
 lemma integral_log_from_zero {b : ℝ} : ∫ s in (0)..b, log s = b * log b - b := by
-    rcases lt_trichotomy b 0 with h | h | h
-    · -- If t is negative, use that log is an even function to reduce to the positive case.
-      conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]
-      rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
-        integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]
-      ring
-    · simp [h]
-    · exact integral_log_from_zero_of_pos h
+  rcases lt_trichotomy b 0 with h | h | h
+  · -- If t is negative, use that log is an even function to reduce to the positive case.
+    conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]
+    rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
+      integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]
+    ring
+  · simp [h]
+  · exact integral_log_from_zero_of_pos h
 
 @[simp]
 theorem integral_log : ∫ s in a..b, log s = b * log b - a * log a - b + a := by
diff --git a/Mathlib/CategoryTheory/Comma/Final.lean b/Mathlib/CategoryTheory/Comma/Final.lean
@@ -104,13 +104,15 @@ end NonSmall
 
 /-- Let the following diagram commute up to isomorphism:
 
+```
       L       R
   A  ---→ T  ←--- B
   |       |       |
   | F     | H     | G
   ↓       ↓       ↓
   A' ---→ T' ←--- B'
       L'      R'
+```
 
 Let `F`, `G`, `R` and `R'` be final and `B` be filtered. Then, the induced functor between the comma
 categories of the first and second row of the diagram is final. -/
diff --git a/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean b/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
@@ -30,8 +30,8 @@ variable {A : Type u₁} [SmallCategory A] {B : Type u₁} [SmallCategory B]
 variable {T : Type u₁} [SmallCategory T]
 
 private lemma isFiltered_of_isFiltered_costructuredArrow_small (L : A ⥤ T) (R : B ⥤ T)
-    [IsFiltered B] [Final R] [∀ b, IsFiltered (CostructuredArrow L (R.obj b))] : IsFiltered A :=
-  isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨by
+    [IsFiltered B] [Final R] [∀ b, IsFiltered (CostructuredArrow L (R.obj b))] : IsFiltered A := by
+  refine isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩
   let R' := Grothendieck.pre (CostructuredArrow.functor L) R
   haveI : ∀ b, PreservesLimitsOfShape J
       (colim (J := (R ⋙ CostructuredArrow.functor L).obj b) (C := Type u₁)) := fun b => by
@@ -43,7 +43,7 @@ private lemma isFiltered_of_isFiltered_costructuredArrow_small (L : A ⥤ T) (R
     colim.map ?_ ≫
     colimit.pre _ R' ≫
     (colimitIsoColimitGrothendieck L (limit F)).inv
-  exact (limitCompWhiskeringLeftIsoCompLimit F (R' ⋙ CostructuredArrow.grothendieckProj L)).hom⟩
+  exact (limitCompWhiskeringLeftIsoCompLimit F (R' ⋙ CostructuredArrow.grothendieckProj L)).hom
 
 end Small
 
diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -656,10 +656,10 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t
     _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity
 
 lemma le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := by
-    rw [le_inv_mul_iff₀ hc]
-    calc c * x
-    _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
-    _ ≤ _ := Real.add_one_le_exp (c * x)
+  rw [le_inv_mul_iff₀ hc]
+  calc c * x
+  _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
+  _ ≤ _ := Real.add_one_le_exp (c * x)
 
 end Real
 
diff --git a/Mathlib/Data/Matroid/Basic.lean b/Mathlib/Data/Matroid/Basic.lean
@@ -709,7 +709,7 @@ theorem Base.exists_insert_of_ssubset (hB : M.Base B) (hIB : I ⊂ B) (hB' : M.B
 
 theorem ext_iff_indep {M₁ M₂ : Matroid α} :
     M₁ = M₂ ↔ (M₁.E = M₂.E) ∧ ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I) :=
-⟨fun h ↦ by (subst h; simp), fun h ↦ ext_indep h.1 h.2⟩
+  ⟨fun h ↦ by (subst h; simp), fun h ↦ ext_indep h.1 h.2⟩
 
 @[deprecated (since := "2024-12-25")] alias eq_iff_indep_iff_indep_forall := ext_iff_indep
 
diff --git a/Mathlib/Data/Matroid/Restrict.lean b/Mathlib/Data/Matroid/Restrict.lean
@@ -458,7 +458,7 @@ theorem Indep.augment (hI : M.Indep I) (hJ : M.Indep J) (hIJ : I.encard < J.enca
 
 lemma Indep.augment_finset {I J : Finset α} (hI : M.Indep I) (hJ : M.Indep J)
     (hIJ : I.card < J.card) : ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e I) := by
-  obtain ⟨x, hx, hxI⟩ := hI.augment hJ (by simpa [encard_eq_coe_toFinset_card] )
+  obtain ⟨x, hx, hxI⟩ := hI.augment hJ (by simpa [encard_eq_coe_toFinset_card])
   simp only [mem_diff, Finset.mem_coe] at hx
   exact ⟨x, hx.1, hx.2, hxI⟩
 
diff --git a/Mathlib/FieldTheory/Galois/Infinite.lean b/Mathlib/FieldTheory/Galois/Infinite.lean
@@ -57,24 +57,24 @@ open Pointwise FiniteGaloisIntermediateField AlgEquiv
 
 lemma fixingSubgroup_isClosed (L : IntermediateField k K) [IsGalois k K] :
     IsClosed (L.fixingSubgroup : Set (K ≃ₐ[k] K)) where
-    isOpen_compl := isOpen_iff_mem_nhds.mpr fun σ h => by
-      apply mem_nhds_iff.mpr
-      rcases Set.not_subset.mp ((mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mp h) with ⟨y, yL, ne⟩
-      use σ • ((adjoin k {y}).1.fixingSubgroup : Set (K ≃ₐ[k] K))
-      constructor
-      · intro f hf
-        rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩
-        simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]
-        apply (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mpr
-        push_neg
-        use y
-        simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]
-        have : g y = y := (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mp hg y <|
-          adjoin_simple_le_iff.mp le_rfl
-        simpa only [this, ne_eq, AlgEquiv.smul_def] using ne
-      · simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]
-        use 1
-        simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]
+  isOpen_compl := isOpen_iff_mem_nhds.mpr fun σ h => by
+    apply mem_nhds_iff.mpr
+    rcases Set.not_subset.mp ((mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mp h) with ⟨y, yL, ne⟩
+    use σ • ((adjoin k {y}).1.fixingSubgroup : Set (K ≃ₐ[k] K))
+    constructor
+    · intro f hf
+      rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩
+      simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]
+      apply (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mpr
+      push_neg
+      use y
+      simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]
+      have : g y = y := (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mp hg y <|
+        adjoin_simple_le_iff.mp le_rfl
+      simpa only [this, ne_eq, AlgEquiv.smul_def] using ne
+    · simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]
+      use 1
+      simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]
 
 lemma fixedField_fixingSubgroup (L : IntermediateField k K) [IsGalois k K] :
     IntermediateField.fixedField L.fixingSubgroup = L := by
@@ -119,7 +119,7 @@ lemma restrict_fixedField (H : Subgroup (K ≃ₐ[k] K)) (L : IntermediateField
     nth_rw 2 [← (h.out.1 ⟨σ, hσ⟩)]
     exact AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩
   · have xL := lift_le _ h
-    apply (mem_lift (⟨x,xL⟩ : L)).mp at h
+    apply (mem_lift (⟨x, xL⟩ : L)).mp at h
     simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp,
       forall_apply_eq_imp_iff₂] at h
     simp only [coe_inf, Set.mem_inter_iff, SetLike.mem_coe, mem_fixedField_iff, xL, and_true]
@@ -221,7 +221,7 @@ theorem isOpen_iff_finite (L : IntermediateField k K) [IsGalois k K] :
     finiteDimensional := normalClosure.is_finiteDimensional k M K
     isGalois := IsGalois.normalClosure k M K }
   have : L ≤ L'.1 := by
-    apply LE.le.trans _ (IntermediateField.le_normalClosure M)
+    apply le_trans _ (IntermediateField.le_normalClosure M)
     rw [←  fixedField_fixingSubgroup M, IntermediateField.le_iff_le]
     exact sub
   let _ : Algebra L L'.1 := RingHom.toAlgebra (IntermediateField.inclusion this)
diff --git a/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean b/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
@@ -13,7 +13,7 @@ This file proves properties of 2×2 block matrices `[A B; C D]` that relate to t
 `D - C*A⁻¹*B`.
 
 Some of the results here generalize to 2×2 matrices in a category, rather than just a ring. A few
-results in this direction can be found in the file `CategoryTheory.Preadditive.Biproducts`,
+results in this direction can be found in the file `Mathlib.CategoryTheory.Preadditive.Biproducts`,
 especially the declarations `CategoryTheory.Biprod.gaussian` and `CategoryTheory.Biprod.isoElim`.
 Compare with `Matrix.invertibleOfFromBlocks₁₁Invertible`.
 
diff --git a/Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean b/Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
@@ -181,7 +181,7 @@ lemma exists_basis_basis_of_span_eq_top_of_mem_algebraMap
     replace hv₃ := hv₃.restrict_scalars (R := K) <| by
       simp_rw [← Algebra.algebraMap_eq_smul_one]
       exact FaithfulSMul.algebraMap_injective K L
-    rw [show ((↑) : v → M) = M'.subtype ∘ v' from rfl] at hv₃
+    rw [show ((↑) : v → M) = M'.subtype ∘ v' by ext; simp [v']] at hv₃
     exact hv₃.of_comp
   suffices span K (Set.range v') = ⊤ by
     let e := (Module.Finite.finite_basis b).equivFin
diff --git a/Mathlib/MeasureTheory/Function/L2Space.lean b/Mathlib/MeasureTheory/Function/L2Space.lean
@@ -180,21 +180,13 @@ private theorem add_left' (f f' g : α →₂[μ] E) : ⟪f + f', g⟫ = inner f
   simp_rw [inner_def, ← integral_add (integrable_inner (𝕜 := 𝕜) f g) (integrable_inner f' g),
     ← inner_add_left]
   refine integral_congr_ae ((coeFn_add f f').mono fun x hx => ?_)
-  -- Porting note: was
-  -- congr
-  -- rwa [Pi.add_apply] at hx
-  simp only
-  congr
+  simp only [hx, Pi.add_apply]
 
 private theorem smul_left' (f g : α →₂[μ] E) (r : 𝕜) : ⟪r • f, g⟫ = conj r * inner f g := by
   rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul]
   refine integral_congr_ae ((coeFn_smul r f).mono fun x hx => ?_)
   simp only
   rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]
-  -- Porting note: was
-  -- rw [smul_eq_mul, ← inner_smul_left]
-  -- congr
-  -- rwa [Pi.smul_apply] at hx
 
 instance innerProductSpace : InnerProductSpace 𝕜 (α →₂[μ] E) where
   norm_sq_eq_inner := norm_sq_eq_inner'
diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean
@@ -1072,7 +1072,6 @@ theorem lintegral_coe_eq_integral (f : α → ℝ≥0) (hfi : Integrable (fun x
   rw [ENNReal.ofReal_toReal]
   rw [← lt_top_iff_ne_top]
   convert hfi.hasFiniteIntegral
-  -- Porting note: `convert` no longer unfolds `HasFiniteIntegral`
   simp_rw [hasFiniteIntegral_iff_enorm, NNReal.enorm_eq]
 
 theorem ofReal_integral_eq_lintegral_ofReal {f : α → ℝ} (hfi : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
@@ -398,8 +398,8 @@ lemma intervalIntegrable_of_even₀ (h₁f : ∀ x, f x = f (-x))
 if it is interval integrable (with respect to the volume measure) on every interval of the form
 `0..x`, for positive `x`. -/
 theorem intervalIntegrable_of_even
-  (h₁f : ∀ x, f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (a b : ℝ) :
-  IntervalIntegrable f volume a b :=
+    (h₁f : ∀ x, f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (a b : ℝ) :
+    IntervalIntegrable f volume a b :=
   -- Split integral and apply lemma
   (intervalIntegrable_of_even₀ h₁f h₂f a).symm.trans (b := 0)
     (intervalIntegrable_of_even₀ h₁f h₂f b)
@@ -410,8 +410,8 @@ interval of the form `0..x`, for positive `x`.
 
 See `intervalIntegrable_of_odd` for a stronger result.-/
 lemma intervalIntegrable_of_odd₀
-  (h₁f : ∀ x, -f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (t : ℝ) :
-  IntervalIntegrable f volume 0 t := by
+    (h₁f : ∀ x, -f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (t : ℝ) :
+    IntervalIntegrable f volume 0 t := by
   rcases lt_trichotomy t 0 with h | h | h
   · rw [IntervalIntegrable.iff_comp_neg]
     conv => arg 1; intro t; rw [← h₁f]
@@ -424,8 +424,8 @@ lemma intervalIntegrable_of_odd₀
 iff it is interval integrable (with respect to the volume measure) on every interval of the form
 `0..x`, for positive `x`. -/
 theorem intervalIntegrable_of_odd
-  (h₁f : ∀ x, -f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (a b : ℝ) :
-  IntervalIntegrable f volume a b :=
+    (h₁f : ∀ x, -f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (a b : ℝ) :
+    IntervalIntegrable f volume a b :=
   -- Split integral and apply lemma
   (intervalIntegrable_of_odd₀ h₁f h₂f a).symm.trans (b := 0) (intervalIntegrable_of_odd₀ h₁f h₂f b)
 
diff --git a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
diff --git a/Mathlib/Probability/Moments/IntegrableExpMul.lean b/Mathlib/Probability/Moments/IntegrableExpMul.lean
diff --git a/Mathlib/RingTheory/Binomial.lean b/Mathlib/RingTheory/Binomial.lean
diff --git a/Mathlib/RingTheory/Ideal/Height.lean b/Mathlib/RingTheory/Ideal/Height.lean
diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean
diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean
diff --git a/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
