chore: tidy various files (#17342)

Ruben-VandeVelde · Ruben-VandeVelde · commit 83450e8f973b · 2024-12-20T12:30:17.000Z
diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean
@@ -415,21 +415,17 @@ theorem continuousPart_evalCLM_eq_zero [TopologicalSpace α] [DiscreteTopology 
   calc
     f.continuousPart s = f.continuousPart (s \ {x}) :=
       (continuousPart_apply_diff _ _ _ (countable_singleton x)).symm
-    _ = f (univ \ f.discreteSupport ∩ (s \ {x})) := rfl
+    _ = f (univ \ f.discreteSupport ∩ (s \ {x})) := by simp [continuousPart]
     _ = indicator (univ \ f.discreteSupport ∩ (s \ {x})) 1 x := rfl
     _ = 0 := by simp
 
 theorem toFunctions_toMeasure [MeasurableSpace α] (μ : Measure α) [IsFiniteMeasure μ] (s : Set α)
     (hs : MeasurableSet s) :
     μ.extensionToBoundedFunctions.toBoundedAdditiveMeasure s = (μ s).toReal := by
-  change
-    μ.extensionToBoundedFunctions
-        (ofNormedAddCommGroupDiscrete (indicator s 1) 1 (norm_indicator_le_one s)) =
-      (μ s).toReal
+  simp only [ContinuousLinearMap.toBoundedAdditiveMeasure]
   rw [extensionToBoundedFunctions_apply]
-  · change ∫ x, s.indicator (fun _ => (1 : ℝ)) x ∂μ = _
-    simp [integral_indicator hs]
-  · change Integrable (indicator s 1) μ
+  · simp [integral_indicator hs]
+  · simp only [coe_ofNormedAddCommGroupDiscrete]
     have : Integrable (fun _ => (1 : ℝ)) μ := integrable_const (1 : ℝ)
     apply
       this.mono' (Measurable.indicator (@measurable_const _ _ _ _ (1 : ℝ)) hs).aestronglyMeasurable
diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
@@ -187,21 +187,21 @@ variable {R M}
 
 theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R}
     (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
-    (↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m' :=
-  { mp := fun H => H ▸ (End_isUnit_apply_inv_apply_of_isUnit h m).symm
-    mpr := fun H =>
-      H.symm ▸ by
-        apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
-        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') }
+    (↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m' where
+  mp H := H ▸ (End_isUnit_apply_inv_apply_of_isUnit h m).symm
+  mpr H :=
+    H.symm ▸ by
+      apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
+      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) :
-    m' = (↑h.unit⁻¹ : Module.End S M) m ↔ m = x • m' :=
-  { mp := fun H => H ▸ (End_isUnit_apply_inv_apply_of_isUnit h m).symm
-    mpr := fun H =>
-      H.symm ▸ by
-        apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
-        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm }
+    m' = (↑h.unit⁻¹ : Module.End S M) m ↔ m = x • m' where
+  mp H := H ▸ (End_isUnit_apply_inv_apply_of_isUnit h m).symm
+  mpr H :=
+    H.symm ▸ by
+      apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
+      simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm
 
 end
 
diff --git a/Mathlib/Algebra/Group/Aut.lean b/Mathlib/Algebra/Group/Aut.lean
@@ -18,8 +18,8 @@ The definition of multiplication in the automorphism groups agrees with function
 multiplication in `Equiv.Perm`, and multiplication in `CategoryTheory.End`, but not with
 `CategoryTheory.comp`.
 
-This file is kept separate from `Algebra/Group/Equiv/*` so that `GroupTheory.Perm` is free to use
-equivalences (and other files that use them) before the group structure is defined.
+This file is kept separate from `Mathlib/Algebra/Group/Equiv/*` so that `Mathlib.GroupTheory.Perm`
+is free to use equivalences (and other files that use them) before the group structure is defined.
 
 ## Tags
 
diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean
@@ -18,7 +18,7 @@ subgroup of `E` such that `L` spans `E` over `K`.
 
 A `ℤ`-lattice `L` can be defined in two ways:
 * For `b` a basis of `E`, then `L = Submodule.span ℤ (Set.range b)` is a ℤ-lattice of `E`
-* As an`ℤ-submodule` of `E` with the additional properties:
+* As a `ℤ-submodule` of `E` with the additional properties:
   * `DiscreteTopology L`, that is `L` is discrete
   * `Submodule.span ℝ (L : Set E) = ⊤`, that is `L` spans `E` over `K`.
 
@@ -354,7 +354,7 @@ theorem measure_fundamentalDomain_ne_zero [Finite ι] [MeasurableSpace E] [Borel
     {μ : Measure E} [Measure.IsAddHaarMeasure μ] :
     μ (fundamentalDomain b) ≠ 0 := by
   convert (ZSpan.isAddFundamentalDomain b μ).measure_ne_zero (NeZero.ne μ)
-  exact (inferInstance : VAddInvariantMeasure (span ℤ (Set.range b)).toAddSubgroup E μ)
+  exact inferInstanceAs <| VAddInvariantMeasure (span ℤ (Set.range b)).toAddSubgroup E μ
 
 theorem measure_fundamentalDomain [Fintype ι] [DecidableEq ι] [MeasurableSpace E] (μ : Measure E)
     [BorelSpace E] [Measure.IsAddHaarMeasure μ] (b₀ : Basis ι ℝ E) :
diff --git a/Mathlib/Algebra/Polynomial/BigOperators.lean b/Mathlib/Algebra/Polynomial/BigOperators.lean
@@ -343,7 +343,7 @@ where additionally, the product of the leading coefficients must be nonzero.
 theorem leadingCoeff_multiset_prod :
     t.prod.leadingCoeff = (t.map fun f => leadingCoeff f).prod := by
   rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]
-  rfl
+  simp only [leadingCoeffHom_apply]
 
 /-- The leading coefficient of a product of polynomials is equal to
 the product of the leading coefficients.
diff --git a/Mathlib/Algebra/Ring/Aut.lean b/Mathlib/Algebra/Ring/Aut.lean
@@ -18,8 +18,8 @@ The definition of multiplication in the automorphism group agrees with function
 multiplication in `Equiv.Perm`, and multiplication in `CategoryTheory.End`, but not with
 `CategoryTheory.comp`.
 
-This file is kept separate from `Algebra/Ring/Equiv.lean` so that `GroupTheory.Perm` is free to use
-equivalences (and other files that use them) before the group structure is defined.
+This file is kept separate from `Mathlib/Algebra/Ring/Equiv.lean` so that `Mathlib.GroupTheory.Perm`
+is free to use equivalences (and other files that use them) before the group structure is defined.
 
 ## Tags
 
diff --git a/Mathlib/Algebra/Ring/Subring/IntPolynomial.lean b/Mathlib/Algebra/Ring/Subring/IntPolynomial.lean
@@ -10,23 +10,20 @@ import Mathlib.Algebra.Polynomial.AlgebraMap
 
 Given a field `K` with a subring `R`, in this file we construct a map from polynomials in `K[X]`
 with coefficients in `R` to `R[X]`. We provide several lemmas to deal with
-coefficients, degree, and evaluation of `intPolynomial`.
+coefficients, degree, and evaluation of `Polynomial.int`.
 This is useful when dealing with integral elements in an extension of fields.
 
 # Main Definitions
-* `Polynomial.int` : given a polynomial `P`. in `K[X]` with coefficients in a field `K` with a
-  subring `R` such that all coefficients belong to `R`, `P.int R` is the corresponding polynomial
-  in `R[X]`.
+* `Polynomial.int` : given a polynomial `P` in `K[X]` whose coefficients all belong to a subring `R`
+  of the field `K`, `P.int R` is the corresponding polynomial in `R[X]`.
 -/
 
 variable {K : Type*} [Field K] (R : Subring K)
 
-open Polynomial
-
 open scoped Polynomial
 
 /-- Given a polynomial in `K[X]` such that all coefficients belong to the subring `R`,
-  `intPolynomial` is the corresponding polynomial in `R[X]`. -/
+  `Polynomial.int` is the corresponding polynomial in `R[X]`. -/
 def Polynomial.int (P : K[X]) (hP : ∀ n : ℕ, P.coeff n ∈ R) : R[X] where
   toFinsupp :=
   { support := P.support
diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean
@@ -415,8 +415,7 @@ variable {ι : Type*} [Fintype ι] {e : E} {Fm : ι → Type*}
 lemma FormalMultilinearSeries.radius_pi_le (p : Π i, FormalMultilinearSeries 𝕜 E (Fm i)) (i : ι) :
     (FormalMultilinearSeries.pi p).radius ≤ (p i).radius := by
   apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
-  obtain ⟨C, -, hC⟩ :  ∃ C > 0, ∀ (n : ℕ),
-    ‖pi p n‖ * ↑r' ^ n ≤ C := norm_mul_pow_le_of_lt_radius _ hr'
+  obtain ⟨C, -, hC⟩ : ∃ C > 0, ∀ n, ‖pi p n‖ * ↑r' ^ n ≤ C := norm_mul_pow_le_of_lt_radius _ hr'
   apply le_radius_of_bound _ C (fun n ↦ ?_)
   apply le_trans _ (hC n)
   gcongr
@@ -460,10 +459,12 @@ lemma HasFPowerSeriesWithinOnBall.pi
   hasSum {_} m hy := Pi.hasSum.2 (fun i ↦ (hf i).hasSum m hy)
 
 lemma hasFPowerSeriesWithinOnBall_pi_iff (hr : 0 < r) :
-    HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r
-      ↔ ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r :=
-  ⟨fun h i ↦ ⟨h.r_le.trans (FormalMultilinearSeries.radius_pi_le _ _), hr,
-    fun m hy ↦ Pi.hasSum.1 (h.hasSum m hy) i⟩, fun h ↦ .pi h hr⟩
+    HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r ↔
+      ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r where
+  mp h i :=
+    ⟨h.r_le.trans (FormalMultilinearSeries.radius_pi_le _ _), hr,
+      fun m hy ↦ Pi.hasSum.1 (h.hasSum m hy) i⟩
+  mpr h := .pi h hr
 
 lemma HasFPowerSeriesOnBall.pi
     (hf : ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r) (hr : 0 < r) :
@@ -472,8 +473,8 @@ lemma HasFPowerSeriesOnBall.pi
   exact HasFPowerSeriesWithinOnBall.pi hf hr
 
 lemma hasFPowerSeriesOnBall_pi_iff (hr : 0 < r) :
-    HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r
-      ↔ ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r := by
+    HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r ↔
+      ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r := by
   simp_rw [← hasFPowerSeriesWithinOnBall_univ]
   exact hasFPowerSeriesWithinOnBall_pi_iff hr
 
@@ -486,8 +487,8 @@ lemma HasFPowerSeriesWithinAt.pi
   exact ⟨r, HasFPowerSeriesWithinOnBall.pi hr r_pos⟩
 
 lemma hasFPowerSeriesWithinAt_pi_iff :
-    HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e
-      ↔ ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e := by
+    HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e ↔
+      ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e := by
   refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
   obtain ⟨r, hr⟩ := h
   exact ⟨r, (hasFPowerSeriesWithinOnBall_pi_iff hr.r_pos).1 hr i⟩
@@ -499,8 +500,8 @@ lemma HasFPowerSeriesAt.pi
   exact HasFPowerSeriesWithinAt.pi hf
 
 lemma hasFPowerSeriesAt_pi_iff :
-    HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e
-      ↔ ∀ i, HasFPowerSeriesAt (f i) (p i) e := by
+    HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e ↔
+      ∀ i, HasFPowerSeriesAt (f i) (p i) e := by
   simp_rw [← hasFPowerSeriesWithinAt_univ]
   exact hasFPowerSeriesWithinAt_pi_iff
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
@@ -270,7 +270,7 @@ lemma Real.HasSum_rexp_HasProd (f : ι → α → ℝ) (hfn : ∀ x n, 0 < f n x
 product.-/
 lemma Real.rexp_tsum_eq_tprod (f : ι → α → ℝ) (hfn : ∀ x n, 0 < f n x)
     (hf : ∀ x : α, Summable fun n => log ((f n x))) :
-      (rexp ∘ (fun a : α => (∑' n : ι, log (f n a)))) = (fun a : α => ∏' n : ι, (f n a)) := by
+    (rexp ∘ (fun a : α => (∑' n : ι, log (f n a)))) = (fun a : α => ∏' n : ι, (f n a)) := by
   ext a
   apply (HasProd.tprod_eq ?_).symm
   apply ((hf a).hasSum.rexp).congr
@@ -279,15 +279,15 @@ lemma Real.rexp_tsum_eq_tprod (f : ι → α → ℝ) (hfn : ∀ x n, 0 < f n x)
   exact funext fun x ↦ exp_log (hfn a x)
 
 lemma Real.summable_cexp_multipliable (f : ι → α → ℝ) (hfn : ∀ x n, 0 < f n x)
-    (hf : ∀ x : α, Summable fun n => log (f n x)) (a : α): Multipliable fun b ↦ f b a := by
+    (hf : ∀ x : α, Summable fun n => log (f n x)) (a : α) : Multipliable fun b ↦ f b a := by
   have := (Real.HasSum_rexp_HasProd f hfn fun a => (hf a).hasSum) a
   use (∏' n : ι, (f n a))
 
 open Complex
 
 lemma Complex.HasSum_cexp_HasProd (f : ι → α → ℂ) (hfn : ∀ x n, f n x ≠ 0)
     (hf : ∀ x : α, HasSum (fun n => log (f n x)) (∑' i, log (f i x))) (a : α) :
-       HasProd (fun b ↦ f b a) (∏' n : ι, (f n a)) := by
+    HasProd (fun b ↦ f b a) (∏' n : ι, (f n a)) := by
   have : HasProd (fun b ↦ f b a) ((cexp ∘ fun a ↦ ∑' (n : ι), log (f n a)) a) := by
     apply ((hf a).cexp).congr
     intro _
@@ -296,16 +296,16 @@ lemma Complex.HasSum_cexp_HasProd (f : ι → α → ℂ) (hfn : ∀ x n, f n x
   rwa [HasProd.tprod_eq this]
 
 lemma Complex.summable_cexp_multipliable (f : ι → α → ℂ) (hfn : ∀ x n, f n x ≠ 0)
-    (hf : ∀ x : α, Summable fun n => log (f n x)) (a : α):
-      Multipliable fun b ↦ f b a := by
+    (hf : ∀ x : α, Summable fun n => log (f n x)) (a : α) :
+    Multipliable fun b ↦ f b a := by
   have := (Complex.HasSum_cexp_HasProd f hfn fun a => (hf a).hasSum) a
   use (∏' n : ι, (f n a))
 
 /--The exponential of a infinite sum of comples logs (which converges absolutely) is an infinite
 product.-/
 lemma Complex.cexp_tsum_eq_tprod (f : ι → α → ℂ) (hfn : ∀ x n, f n x ≠ 0)
     (hf : ∀ x : α, Summable fun n => log (f n x)) :
-      (cexp ∘ (fun a : α => (∑' n : ι, log (f n a)))) = (fun a : α => ∏' n : ι, ((f n a))) := by
+    (cexp ∘ (fun a : α => (∑' n : ι, log (f n a)))) = fun a : α => ∏' n : ι, f n a := by
   ext a
   apply (HasProd.tprod_eq ?_).symm
   apply ((hf a).hasSum.cexp).congr
diff --git a/Mathlib/CategoryTheory/Bicategory/Adjunction.lean b/Mathlib/CategoryTheory/Bicategory/Adjunction.lean
@@ -92,8 +92,6 @@ namespace Adjunction
 
 attribute [simp] left_triangle right_triangle
 
--- attribute [local simp] leftZigzag rightZigzag
-
 /-- Adjunction between identities. -/
 def id (a : B) : 𝟙 a ⊣ 𝟙 a where
   unit := (ρ_ _).inv
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
@@ -30,7 +30,7 @@ For an explanation of `Finset` design decisions, please see `Mathlib/Data/Finset
 
 ### Equivalences between finsets
 
-* The `Mathlib/Logic/Equiv/Defs.lean` files describe a general type of equivalence, so look in there
+* The `Mathlib/Logic/Equiv/Defs.lean` file describes a general type of equivalence, so look in there
   for any lemmas. There is some API for rewriting sums and products from `s` to `t` given that
   `s ≃ t`.
   TODO: examples
diff --git a/Mathlib/Data/Finsupp/Weight.lean b/Mathlib/Data/Finsupp/Weight.lean
@@ -24,17 +24,17 @@ We fix a type `σ` and an `AddCommMonoid M`, as well as a function `w : σ → M
 with respect to `w`: it is the sum `∑ (f i) • (w i)`.
 It is an `AddMonoidHom` map defined using `Finsupp.linearCombination`.
 
-- `Finsupp.le_weight`says that `f s ≤ f.weight w` when `M = ℕ``
+- `Finsupp.le_weight` says that `f s ≤ f.weight w` when `M = ℕ`
 
-- `Finsupp.le_weight_of_nonneg'` says that `w s ≤ f.weight w`
+- `Finsupp.le_weight_of_ne_zero` says that `w s ≤ f.weight w`
 for `OrderedAddCommMonoid M`, when `f s ≠ 0` and all `w i` are nonnegative.
 
-- `Finsupp.le_weight'` is the same statement for `CanonicallyOrderedAddCommMonoid M`.
+- `Finsupp.le_weight_of_ne_zero'` is the same statement for `CanonicallyOrderedAddCommMonoid M`.
 
 - `NonTorsionWeight`: all values `w s` are non torsion in `M`.
 
 - `Finsupp.weight_eq_zero_iff_eq_zero` says that `f.weight w = 0` iff
-`f = 0` for `NonTorsion Weight w` and `CanonicallyOrderedAddCommMonoid M`.
+`f = 0` for `NonTorsionWeight w` and `CanonicallyOrderedAddCommMonoid M`.
 
 - For `w : σ → ℕ` and `Finite σ`, `Finsupp.finite_of_nat_weight_le` proves that
 there are finitely many `f : σ →₀ ℕ` of bounded weight.
@@ -75,7 +75,7 @@ section AddCommMonoid
 
 variable [AddCommMonoid M]
 /-- The `weight` of the finitely supported function `f : σ →₀ ℕ`
-with respect to `w : σ → M` is the sum `∑(f i)•(w i)`. -/
+with respect to `w : σ → M` is the sum `∑ i, f i • w i`. -/
 noncomputable def weight : (σ →₀ ℕ) →+ M :=
   (Finsupp.linearCombination ℕ w).toAddMonoidHom
 
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -1284,7 +1284,7 @@ theorem foldl_eq_of_comm_of_assoc [hcomm : Std.Commutative f] [hassoc : Std.Asso
   | a, b, c :: l => by
     simp only [foldl_cons]
     have : RightCommutative f := inferInstance
-    rw [← foldl_eq_of_comm_of_assoc .., this.right_comm]; rfl
+    rw [← foldl_eq_of_comm_of_assoc .., this.right_comm, foldl_cons]
 
 theorem foldl_eq_foldr [Std.Commutative f] [Std.Associative f] :
     ∀ a l, foldl f a l = foldr f a l
diff --git a/Mathlib/Data/Matrix/RowCol.lean b/Mathlib/Data/Matrix/RowCol.lean
@@ -136,7 +136,7 @@ theorem row_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α
   ext
   rfl
 
-theorem row_mulVec_eq_const [Fintype m] [NonUnitalNonAssocSemiring α]  (v w : m → α) :
+theorem row_mulVec_eq_const [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :
     Matrix.row ι v *ᵥ w = Function.const _ (v ⬝ᵥ w) := rfl
 
 theorem mulVec_col_eq_const [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :
diff --git a/Mathlib/Data/Nat/Choose/Sum.lean b/Mathlib/Data/Nat/Choose/Sum.lean
@@ -133,8 +133,8 @@ theorem sum_Icc_choose (n k : ℕ) : ∑ m ∈ Icc k n, m.choose k = (n + 1).cho
   · induction n, h using le_induction with
     | base => simp
     | succ n _ ih =>
-      rw [← Ico_insert_right (by omega), sum_insert (by simp),
-        show Ico k (n + 1) = Icc k n by rfl, ih, choose_succ_succ' (n + 1)]
+      rw [← Ico_insert_right (by omega), sum_insert (by simp), Ico_succ_right, ih,
+        choose_succ_succ' (n + 1)]
 
 /-- **Zhu Shijie's identity** aka hockey-stick identity, version with `range`.
 Summing `(i + k).choose k` for `i ∈ [0, n]` gives `(n + k + 1).choose (k + 1)`.
diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
@@ -648,7 +648,6 @@ lemma one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) :=
  | 0 => by simp [Nat.zero_pow (Nat.pos_of_ne_zero hn)]
  | 1 => by simp
  | a + 2 => by simp [one_lt_pow hn]
-  -- one_lt_pow_iff_of_nonneg (zero_le _) h
 
 lemma one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) := one_lt_pow n.succ_ne_zero (by decide)
 
diff --git a/Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean b/Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
@@ -11,7 +11,7 @@ import Mathlib.MeasureTheory.Measure.Haar.Unique
 # Ergodicity from minimality
 
 In this file we prove that the left shift `(a * ·)` on a compact topological group `G`
-is ergodic with respect to the Haar measure if and only if its minimal,
+is ergodic with respect to the Haar measure if and only if it is minimal,
 i.e., the powers `a ^ n` are dense in `G`.
 
 The proof of the more difficult "if minimal, then ergodic" implication
diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
@@ -999,11 +999,13 @@ theorem finrank_eq_one_iff : finrank F K = 1 ↔ K = ⊥ := by
   rw [← toSubalgebra_eq_iff, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
     bot_toSubalgebra]
 
-@[simp] protected
-theorem rank_bot : Module.rank F (⊥ : IntermediateField F E) = 1 := by rw [rank_eq_one_iff]
+@[simp]
+protected theorem rank_bot : Module.rank F (⊥ : IntermediateField F E) = 1 := by
+  rw [rank_eq_one_iff]
 
-@[simp] protected
-theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1 := by rw [finrank_eq_one_iff]
+@[simp]
+protected theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1 := by
+  rw [finrank_eq_one_iff]
 
 @[simp] theorem rank_bot' : Module.rank (⊥ : IntermediateField F E) E = Module.rank F E := by
   rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean
@@ -503,8 +503,7 @@ theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} :
 
 lemma cycleOf_ne_one_iff_mem_cycleFactorsFinset {g : Equiv.Perm α} {x : α} :
     g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset := by
-  rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.mem_support,
-        ne_eq, Equiv.Perm.cycleOf_eq_one_iff]
+  rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]
 
 theorem mem_cycleFactorsFinset_support_le {p f : Perm α} (h : p ∈ cycleFactorsFinset f) :
     p.support ≤ f.support := by
diff --git a/Mathlib/GroupTheory/Perm/Finite.lean b/Mathlib/GroupTheory/Perm/Finite.lean
@@ -14,7 +14,7 @@ import Mathlib.Data.Finite.Sum
 # Permutations on `Fintype`s
 
 This file contains miscellaneous lemmas about `Equiv.Perm` and `Equiv.swap`, building on top
-of those in `Logic/Equiv/Basic.lean` and other files in `GroupTheory/Perm/*`.
+of those in `Mathlib/Logic/Equiv/Basic.lean` and other files in `Mathlib/GroupTheory/Perm/*`.
 -/
 
 universe u v
diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
@@ -1280,7 +1280,7 @@ span. -/
 lemma affineSpan_le_toAffineSubspace_span {s : Set V} :
     affineSpan k s ≤ (Submodule.span k s).toAffineSubspace := by
   intro x hx
-  show x ∈ Submodule.span k s
+  simp only [SetLike.mem_coe, Submodule.mem_toAffineSubspace]
   induction hx using affineSpan_induction' with
   | mem x hx => exact Submodule.subset_span hx
   | smul_vsub_vadd c u _ v _ w _ hu hv hw =>
diff --git a/Mathlib/LinearAlgebra/Vandermonde.lean b/Mathlib/LinearAlgebra/Vandermonde.lean
@@ -187,8 +187,7 @@ theorem eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials {n : ℕ
   rw [sum_eq_of_subset _ (fun j => zero_mul ((v i) ^ j)) this, ← Fin.sum_univ_eq_sum_range]
   congr
   ext k
-  rw [mul_comm, Matrix.of_apply, RingHom.id_apply]
-  rfl
+  rw [mul_comm, Matrix.of_apply, RingHom.id_apply, of_apply]
 
 theorem det_eval_matrixOfPolynomials_eq_det_vandermonde {n : ℕ} (v : Fin n → R) (p : Fin n → R[X])
     (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) :
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
diff --git a/Mathlib/NumberTheory/VonMangoldt.lean b/Mathlib/NumberTheory/VonMangoldt.lean
diff --git a/Mathlib/Order/Defs/LinearOrder.lean b/Mathlib/Order/Defs/LinearOrder.lean
diff --git a/Mathlib/Order/Partition/Finpartition.lean b/Mathlib/Order/Partition/Finpartition.lean
diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean
diff --git a/Mathlib/RingTheory/Norm/Basic.lean b/Mathlib/RingTheory/Norm/Basic.lean
diff --git a/Mathlib/RingTheory/Presentation.lean b/Mathlib/RingTheory/Presentation.lean
diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/Mathlib/Topology/Order/ScottTopology.lean
