chore: tidy various files (#31207)

Ruben-VandeVelde · Ruben-VandeVelde · commit a79df06b3d23 · 2025-11-03T21:57:47.000Z
diff --git a/Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean b/Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean
@@ -38,7 +38,7 @@ noncomputable instance : Module R (Ext X Y n) :=
 
 lemma smul_eq_comp_mk₀ (x : Ext X Y n) (r : R) :
     r • x = x.comp (mk₀ (r • 𝟙 Y)) (add_zero _) := by
-  letI := HasDerivedCategory.standard C
+  let := HasDerivedCategory.standard C
   ext
   apply ((Equiv.linearEquiv R homEquiv).map_smul r x).trans
   change r • homEquiv x = (x.comp (mk₀ (r • 𝟙 Y)) (add_zero _)).hom
@@ -54,14 +54,14 @@ lemma smul_hom (x : Ext X Y n) (r : R) [HasDerivedCategory C] :
 lemma comp_smul {X Y Z : C} {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b)
     {c : ℕ} (h : a + b = c) (r : R) :
     α.comp (r • β) h = r • α.comp β h := by
-  letI := HasDerivedCategory.standard C
+  let := HasDerivedCategory.standard C
   aesop
 
 @[simp]
 lemma smul_comp {X Y Z : C} {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b)
     {c : ℕ} (h : a + b = c) (r : R) :
     (r • α).comp β h = r • α.comp β h := by
-  letI := HasDerivedCategory.standard C
+  let := HasDerivedCategory.standard C
   aesop
 
 open DerivedCategory in
@@ -76,7 +76,7 @@ noncomputable def homLinearEquiv [HasDerivedCategory.{w'} C] :
   map_smul' := by simp
 
 lemma mk₀_smul (r : R) (f : X ⟶ Y) : mk₀ (r • f) = r • mk₀ f := by
-  letI := HasDerivedCategory.standard C
+  let := HasDerivedCategory.standard C
   aesop
 
 /-- The linear equivalence `Ext X Y 0 ≃ₜ[R] (X ⟶ Y)`. -/
diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean
@@ -340,8 +340,8 @@ lemma IsUnit.conjugate_nonneg_iff {u x : R} (hu : IsUnit u) :
     0 ≤ u * x * star u ↔ 0 ≤ x := by
   refine ⟨fun h ↦ ?_, fun h ↦ conjugate_nonneg' h _⟩
   obtain ⟨v, hv⟩ := hu.exists_left_inv
-  have := by simpa [← mul_assoc] using conjugate_nonneg' h v
-  rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
+  have : 0 ≤ (v * u) * x * star (v * u) := by simpa [mul_assoc] using conjugate_nonneg' h v
+  simpa [hv]
 
 lemma IsUnit.conjugate_nonneg_iff' {u x : R} (hu : IsUnit u) :
     0 ≤ star u * x * u ↔ 0 ≤ x := by
diff --git a/Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean b/Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean
@@ -23,7 +23,7 @@ variable {A B : Type*} [Semiring A] [Algebra k A] [Semiring B] [Algebra k B]
 
 /-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom` -/
 def liftNCAlgHom [MulSemiringAction G A] [SMulCommClass G k A] (f : A →ₐ[k] B)
-  (g : G →* B) (h_comm : ∀ {x y}, (f (y • x)) * g y = (g y) * (f x)) :
+    (g : G →* B) (h_comm : ∀ {x y}, (f (y • x)) * g y = (g y) * (f x)) :
     SkewMonoidAlgebra A G →ₐ[k] B where
   __ := liftNCRingHom (f : A →+* B) g h_comm
   commutes' := by simp [liftNCRingHom]
diff --git a/Mathlib/Algebra/SkewPolynomial/Basic.lean b/Mathlib/Algebra/SkewPolynomial/Basic.lean
@@ -135,7 +135,7 @@ lemma φ_iterate_apply (n : ℕ) (a : R) : (φ^[n] a) = ((ofAdd n) • a) := by
   induction n with
   | zero => simp
   | succ n hn =>
-      simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
+    simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
       ← mul_smul, mul_comm]
 
 end phi
@@ -145,8 +145,8 @@ def monomial (n : ℕ) : R →ₗ[R] SkewPolynomial R := lsingle (ofAdd n)
 
 lemma monomial_zero_right (n : ℕ) : monomial n (0 : R) = 0 := single_zero _
 
-lemma monomial_zero_one [MulSemiringAction (Multiplicative ℕ) R] :
-  monomial (0 : ℕ) (1 : R) = 1 := by rfl
+lemma monomial_zero_one [MulSemiringAction (Multiplicative ℕ) R] : monomial (0 : ℕ) (1 : R) = 1 :=
+  rfl
 
 lemma monomial_def (n : ℕ) (a : R) : monomial n a = single (ofAdd n) a := rfl
 
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean
@@ -13,7 +13,7 @@ we say that `x` is uniquely a `1`-codimensional face of `y` if there
 exists a unique `i : Fin (d + 2)` such that `X.δ i y = x`. In this file,
 we extend this to a predicate `IsUniquelyCodimOneFace` involving two terms
 in the type `X.S` of simplices of `X`. This is used in the
-file `AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing` for the
+file `Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean` for the
 study of strong (inner) anodyne extensions.
 
 ## References
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean
@@ -47,7 +47,8 @@ variable {X : SSet.{u}} (A : X.Subcomplex)
 /-- A pairing for a subcomplex `A` of a simplicial set `X` consists of a partition
 of the nondegenerate simplices of `X` not in `A` in two types (I) and (II) of simplices,
 and a bijection between the type (II) simplices and the type (I) simplices.
-See the introduction of the file `AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing`. -/
+See the introduction of the file
+`Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean`. -/
 structure Pairing where
   /-- the set of type (I) simplices -/
   I : Set A.N
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean b/Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
@@ -575,7 +575,7 @@ instance preservesBinaryProduct (X Y : SSet) :
 `Discrete Limits.WalkingPair`. -/
 instance preservesBinaryProducts :
     PreservesLimitsOfShape (Discrete Limits.WalkingPair) hoFunctor where
-  preservesLimit {F} := preservesLimit_of_iso_diagram hoFunctor (id (diagramIsoPair F).symm)
+  preservesLimit {F} := preservesLimit_of_iso_diagram hoFunctor (diagramIsoPair F).symm
 
 /-- The functor `hoFunctor : SSet ⥤ Cat` preserves finite products of simplicial sets. -/
 instance preservesFiniteProducts : PreservesFiniteProducts hoFunctor :=
diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/ConvergenceOnBall.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/ConvergenceOnBall.lean
@@ -54,4 +54,4 @@ theorem AnalyticOn.hasFPowerSeriesOnBall :
     0 < p.radius → AnalyticOn 𝕜 f (EMetric.ball x p.radius) →
     HasFPowerSeriesOnBall f p x p.radius := by
   intro hr hs
-  exact hs.hasFPowerSeriesOnSubball hr (by rfl)
+  exact hs.hasFPowerSeriesOnSubball hr le_rfl
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
@@ -531,7 +531,7 @@ def _root_.HasCompactSupport.toSchwartzMap {f : E → F} (h₁ : HasCompactSuppo
     set g := fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖
     have hg₁ : Continuous g := by
       apply Continuous.mul (by fun_prop)
-      exact (h₂.of_le (right_eq_inf.mp rfl)).continuous_iteratedFDeriv'.norm
+      exact (h₂.of_le (mod_cast le_top)).continuous_iteratedFDeriv'.norm
     have hg₂ : HasCompactSupport g := (h₁.iteratedFDeriv _).norm.mul_left
     obtain ⟨x₀, hx₀⟩ := hg₁.exists_forall_ge_of_hasCompactSupport hg₂
     exact ⟨g x₀, hx₀⟩
diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean
@@ -431,7 +431,7 @@ theorem hasSum_sq_fourierCoeffOn
     {a b : ℝ} {f : ℝ → ℂ} (hab : a < b) (hL2 : MemLp f 2 (volume.restrict (Ioc a b))) :
     HasSum (fun i => ‖fourierCoeffOn hab f i‖ ^ 2) ((b - a)⁻¹ • ∫ x in a..b, ‖f x‖ ^ 2) := by
   haveI := Fact.mk (by linarith : 0 < b - a)
-  rw [←add_sub_cancel a b] at hL2
+  rw [← add_sub_cancel a b] at hL2
   have h := hL2.memLp_liftIoc.haarAddCircle
   convert hasSum_sq_fourierCoeff h.toLp using 1
   · simp [fourierCoeff_congr_ae h.coeFn_toLp, fourierCoeff_liftIoc_eq]
diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
@@ -288,18 +288,8 @@ theorem WithSeminorms.hasBasis_zero_ball (hp : WithSeminorms p) :
     (𝓝 (0 : E)).HasBasis
     (fun sr : Finset ι × ℝ => 0 < sr.2) fun sr => (sr.1.sup p).ball 0 sr.2 := by
   refine ⟨fun V => ?_⟩
-  simp only [hp.hasBasis.mem_iff, SeminormFamily.basisSets_iff, Prod.exists]
-  #adaptation_note
-  /--
-  nightly-2025-09-21
-  `grind` is failing here
-  Minimised in https://github.com/leanprover/lean4/pull/10497
-  -/
-  constructor
-  · rintro ⟨-, ⟨s, r, hr, rfl⟩, hV⟩
-    exact ⟨s, r, hr, hV⟩
-  · rintro ⟨s, r, hr, hV⟩
-    exact ⟨_, ⟨s, r, hr, rfl⟩, hV⟩
+  simp only [hp.hasBasis.mem_iff, SeminormFamily.basisSets_iff, Prod.exists, id_eq]
+  grind
 
 theorem WithSeminorms.hasBasis_ball (hp : WithSeminorms p) {x : E} :
     (𝓝 (x : E)).HasBasis
diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean
@@ -130,7 +130,7 @@ protected lemma posPart_add_negPart (a : A) (ha : IsSelfAdjoint a := by cfc_tac)
   exact cfcₙ_congr fun x hx ↦ posPart_add_negPart x
 
 lemma abs_sub_self (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : abs a - a = 2 • a⁻ := by
- simpa [two_smul] using
+  simpa [two_smul] using
     congr($(CFC.posPart_add_negPart a) - $(CFC.posPart_sub_negPart a)).symm
 
 lemma abs_add_self (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : abs a + a = 2 • a⁺ := by
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Opposites/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Opposites/Equalizers.lean
@@ -49,19 +49,19 @@ def parallelPairOpIso {X Y : C} (f g : X ⟶ Y) :
 
 @[simp]
 lemma parallelPairOpIso_hom_app_zero {X Y : C} (f g : X ⟶ Y) :
-  (parallelPairOpIso f g).hom.app WalkingParallelPair.zero = 𝟙 _ := rfl
+    (parallelPairOpIso f g).hom.app WalkingParallelPair.zero = 𝟙 _ := rfl
 
 @[simp]
 lemma parallelPairOpIso_hom_app_one {X Y : C} (f g : X ⟶ Y) :
-  (parallelPairOpIso f g).hom.app WalkingParallelPair.one = 𝟙 _ := rfl
+    (parallelPairOpIso f g).hom.app WalkingParallelPair.one = 𝟙 _ := rfl
 
 @[simp]
 lemma parallelPairOpIso_inv_app_zero {X Y : C} (f g : X ⟶ Y) :
-  (parallelPairOpIso f g).inv.app WalkingParallelPair.zero = 𝟙 _ := rfl
+    (parallelPairOpIso f g).inv.app WalkingParallelPair.zero = 𝟙 _ := rfl
 
 @[simp]
 lemma parallelPairOpIso_inv_app_one {X Y : C} (f g : X ⟶ Y) :
-  (parallelPairOpIso f g).inv.app WalkingParallelPair.one = 𝟙 _ := rfl
+    (parallelPairOpIso f g).inv.app WalkingParallelPair.one = 𝟙 _ := rfl
 
 /-- The canonical isomorphism relating `(parallelPair f g).op` and `parallelPair f.op g.op` -/
 def opParallelPairIso {X Y : C} (f g : X ⟶ Y) :
@@ -77,19 +77,23 @@ def opParallelPairIso {X Y : C} (f g : X ⟶ Y) :
 
 @[simp]
 lemma opParallelPairIso_hom_app_zero {X Y : C} (f g : X ⟶ Y) :
-  (opParallelPairIso f g).hom.app (op WalkingParallelPair.zero) = 𝟙 _ := by simp [opParallelPairIso]
+    (opParallelPairIso f g).hom.app (op WalkingParallelPair.zero) = 𝟙 _ := by
+  simp [opParallelPairIso]
 
 @[simp]
 lemma opParallelPairIso_hom_app_one {X Y : C} (f g : X ⟶ Y) :
-  (opParallelPairIso f g).hom.app (op WalkingParallelPair.one) = 𝟙 _ := by simp [opParallelPairIso]
+    (opParallelPairIso f g).hom.app (op WalkingParallelPair.one) = 𝟙 _ := by
+  simp [opParallelPairIso]
 
 @[simp]
 lemma opParallelPairIso_inv_app_zero {X Y : C} (f g : X ⟶ Y) :
-  (opParallelPairIso f g).inv.app (op WalkingParallelPair.zero) = 𝟙 _ := by simp [opParallelPairIso]
+    (opParallelPairIso f g).inv.app (op WalkingParallelPair.zero) = 𝟙 _ := by
+  simp [opParallelPairIso]
 
 @[simp]
 lemma opParallelPairIso_inv_app_one {X Y : C} (f g : X ⟶ Y) :
-  (opParallelPairIso f g).inv.app (op WalkingParallelPair.one) = 𝟙 _ := by simp [opParallelPairIso]
+    (opParallelPairIso f g).inv.app (op WalkingParallelPair.one) = 𝟙 _ := by
+  simp [opParallelPairIso]
 
 namespace Cofork
 
diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean
@@ -21,20 +21,18 @@ The definition presents it as a natural number.
 * `Nat.uniformBell m n` : short name for `Multiset.bell (replicate m n)`
 
 * `Multiset.bell_mul_eq` shows that
-    `m.bell * (m.map (fun j ↦ j !)).prod *
-      Π j ∈ (m.toFinset.erase 0), (m.count j)! = m.sum !`
+  `m.bell * (m.map (fun j ↦ j !)).prod * Π j ∈ (m.toFinset.erase 0), (m.count j)! = m.sum !`
 
 * `Nat.uniformBell_mul_eq`  shows that
-    `uniformBell m n * n ! ^ m * m ! = (m * n)!`
+  `uniformBell m n * n ! ^ m * m ! = (m * n) !`
 
 * `Nat.uniformBell_succ_left` computes `Nat.uniformBell (m + 1) n` from `Nat.uniformBell m n`
 
 * `Nat.bell n`: the `n`th standard Bell number,
-    which counts the number of partitions of a set of cardinality `n`
+  which counts the number of partitions of a set of cardinality `n`
 
 * `Nat.bell_succ n` shows that
-    `Nat.bell (n + 1) = ∑ k ∈ Finset.range (n + 1),
-      Nat.choose n k * Nat.bell (n - k)`
+  `Nat.bell (n + 1) = ∑ k ∈ Finset.range (n + 1), Nat.choose n k * Nat.bell (n - k)`
 
 ## TODO
 
@@ -190,15 +188,14 @@ protected def bell : ℕ → ℕ
   | n + 1 => ∑ i : Fin n.succ, choose n i * Nat.bell (n - i)
 
 theorem bell_succ (n : ℕ) :
-  Nat.bell (n + 1) = ∑ i : Fin n.succ, Nat.choose n i *
-    Nat.bell (n - i) := by
+    Nat.bell (n + 1) = ∑ i : Fin n.succ, Nat.choose n i * Nat.bell (n - i) := by
   rw [Nat.bell]
 
 theorem bell_succ' (n : ℕ) :
-  Nat.bell (n + 1) =
-    ∑ ij ∈ Finset.antidiagonal n, Nat.choose n ij.1 * Nat.bell ij.2 := by
-  rw [Nat.bell_succ, Finset.Nat.sum_antidiagonal_eq_sum_range_succ
-    (fun x y => Nat.choose n x * Nat.bell y) n, Finset.sum_range]
+    Nat.bell (n + 1) = ∑ ij ∈ Finset.antidiagonal n, Nat.choose n ij.1 * Nat.bell ij.2 := by
+  rw [Nat.bell_succ,
+    Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => Nat.choose n x * Nat.bell y) n,
+    Finset.sum_range]
 
 
 @[simp]
diff --git a/Mathlib/Control/Monad/Cont.lean b/Mathlib/Control/Monad/Cont.lean
@@ -177,10 +177,9 @@ instance [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (OptionT m) where
       bind_congr fun | some _ => rfl | none => by simp [@callCC_dummy m _]
   callCC_bind_left := by
     intros
-    simp only [callCC, OptionT.callCC, OptionT.goto_mkLabel, bind_pure_comp, OptionT.run_bind,
-      OptionT.run_mk, Option.elimM_map, Option.elim_some, @callCC_bind_left m _]
-    ext; rfl
-  callCC_dummy := by intros; simp only [callCC, OptionT.callCC, @callCC_dummy m _]; ext; rfl
+    ext
+    simp [callCC, OptionT.goto_mkLabel, @callCC_bind_left m _]
+  callCC_dummy := by intros; ext; simp [callCC, OptionT.callCC, @callCC_dummy m _]
 
 def WriterT.mkLabel {α β ω} [EmptyCollection ω] : Label (α × ω) m β → Label α (WriterT ω m) β
   | ⟨f⟩ => ⟨fun a => monadLift <| f (a, ∅)⟩
diff --git a/Mathlib/GroupTheory/FreeGroup/Orbit.lean b/Mathlib/GroupTheory/FreeGroup/Orbit.lean
@@ -7,7 +7,7 @@ import Mathlib.GroupTheory.FreeGroup.Reduce
 import Mathlib.GroupTheory.GroupAction.Defs
 
 /-!
-For any `w : α × bool`, `FreeGroup.startsWith w` is the set of all elemenents of `FreeGroup α` that
+For any `w : α × Bool`, `FreeGroup.startsWith w` is the set of all elemenents of `FreeGroup α` that
 start with `w`.
 
 The main theorem `Orbit.duplicate` proves that applying `w⁻¹` to the orbit of `x` under the action
@@ -38,10 +38,8 @@ lemma startsWith.disjoint_iff_ne {w w' : α × Bool} :
   exact Iff.intro (fun h ↦ h (mk [w]) (by simp)) (by grind)
 
 lemma startsWith.Injective : @startsWith α _|>.Injective := fun a b h ↦ by
-  simp only [startsWith, Set.ext_iff, Set.mem_setOf_eq] at *
-  specialize h (mk [a])
-  simp at h
-  exact h
+  simp only [startsWith, Set.ext_iff, Set.mem_setOf_eq] at h
+  simpa using h (mk [a])
 
 theorem startsWith_mk_mul {w : α × Bool} (g : FreeGroup α)
     (h : ¬ g ∈ startsWith (w.1, !w.2)) : mk [w] * g ∈ startsWith w := by
diff --git a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean
@@ -70,8 +70,7 @@ lemma ext_of_lintegral_mul_boundedContinuousFunction [IsFiniteMeasure μ]
   have (z : X × Y) := ENNReal.continuous_coe.tendsto _ |>.comp <|
     (tendsto_pi_nhds.1 (HasOuterApproxClosed.tendsto_apprSeq hs₁) z.1).mul
     (tendsto_pi_nhds.1 (HasOuterApproxClosed.tendsto_apprSeq hs₂) z.2)
-  simp_rw [show (fun _ ↦ 1 : X → ℝ≥0) = 1 from rfl, show (fun _ ↦ 1 : Y → ℝ≥0) = 1 from rfl,
-    ← Set.indicator_prod_one] at this
+  simp_rw [← Pi.one_def, ← Set.indicator_prod_one] at this
   have h1 : Tendsto (fun n ↦ ∫⁻ z, (hs₁.apprSeq n z.1 * hs₂.apprSeq n z.2 : ℝ≥0) ∂μ)
       atTop (𝓝 (∫⁻ z, ((s₁ ×ˢ s₂).indicator 1 z : ℝ≥0) ∂μ)) := by
     refine tendsto_lintegral_filter_of_dominated_convergence 1
diff --git a/Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean b/Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
@@ -48,7 +48,7 @@ theorem associated_norm_zeta_sub_one : Associated (Algebra.norm ℤ (hζ.toInteg
       rw [h, zero_add, pow_one] at hK hζ
       rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
     | succ n =>
-      rw [h, add_assoc, show 1 + 1 = 2 by rfl] at hK hζ
+      rw [h, add_assoc, one_add_one_eq_two] at hK hζ
       rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
   · rw [hζ.norm_toInteger_sub_one_of_prime_ne_two h]
 
diff --git a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
@@ -121,7 +121,7 @@ theorem logEmbedding_eq_zero_iff {x : (𝓞 K)ˣ} :
 theorem logEmbedding_ker : (logEmbedding K).ker = (torsion K).toAddSubgroup := by
   ext x
   rw [AddMonoidHom.mem_ker, ← ofMul_toMul x, logEmbedding_eq_zero_iff]
-  rfl
+  simp
 
 theorem map_logEmbedding_sup_torsion (s : AddSubgroup (Additive (𝓞 K)ˣ)) :
     (s ⊔ (torsion K).toAddSubgroup).map (logEmbedding K) = s.map (logEmbedding K) := by
diff --git a/Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean b/Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean
@@ -20,7 +20,7 @@ where `N` is the norm map sending `a : A` to `∑ ρ(g)(a)` for all `g` in `G`.
 When `G` is generated by `g` and `A` is the left regular representation `k[G]`, this chain complex
 is a projective resolution of `k` as a trivial representation, which we prove here.
 
-In the file `RepresentationTheory/HomologicalComplex/GroupHomology/FiniteCyclic.lean`, we use
+In the file `Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean`, we use
 this resolution to compute the group homology of representations of finite cyclic groups.
 
 ## Main definitions
diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean
@@ -88,8 +88,8 @@ noncomputable def groupHomologyIsoEven
 noncomputable abbrev groupHomologyπEven
     (hg : ∀ x, x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) :
     ModuleCat.of k (LinearMap.ker A.ρ.norm) ⟶ groupHomology A i :=
-    (ShortComplex.moduleCatCyclesIso <| subCompNormHom A g).inv ≫
-      ShortComplex.homologyπ _ ≫ (groupHomologyIsoEven A g hg i hi).inv
+  (ShortComplex.moduleCatCyclesIso <| subCompNormHom A g).inv ≫
+    ShortComplex.homologyπ _ ≫ (groupHomologyIsoEven A g hg i hi).inv
 
 lemma groupHomologyπEven_eq_zero_iff (hg : ∀ x, x ∈ Subgroup.zpowers g)
     (i : ℕ) [NeZero i] (hi : Even i) (x : LinearMap.ker A.ρ.norm) :
@@ -102,7 +102,7 @@ lemma groupHomologyπEven_eq_iff (hg : ∀ x, x ∈ Subgroup.zpowers g)
     (i : ℕ) [NeZero i] (hi : Even i) (x y : LinearMap.ker A.ρ.norm) :
     groupHomologyπEven A g hg i hi x = groupHomologyπEven A g hg i hi y ↔
       x.1 - y.1 ∈ LinearMap.range (applyAsHom A g - 𝟙 A).hom.hom := by
-  rw [← sub_eq_zero, ← map_sub, groupHomologyπEven_eq_zero_iff]; rfl
+  rw [← sub_eq_zero, ← map_sub, groupHomologyπEven_eq_zero_iff, AddSubgroupClass.coe_sub]
 
 /-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `Hⁱ(G, A)` is isomorphic
 to the homology of the short complex of `k`-modules `A --N--> A --(ρ(g) - 𝟙)--> A` when `i` is
@@ -118,8 +118,8 @@ noncomputable def groupHomologyIsoOdd (hg : ∀ x, x ∈ Subgroup.zpowers g) (i
 `Ker(ρ(g) - Id(A)) ⟶ Ker(ρ(g) - Id(A))/Im(N) ≅ Hᵢ(G, A)` for any odd `i`. -/
 noncomputable abbrev groupHomologyπOdd (hg : ∀ x, x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) :
     ModuleCat.of k (LinearMap.ker (applyAsHom A g - 𝟙 A).hom.hom) ⟶ groupHomology A i :=
-    (ShortComplex.moduleCatCyclesIso <| normHomCompSub A g).inv ≫
-      ShortComplex.homologyπ _ ≫ (groupHomologyIsoOdd A g hg i hi).inv
+  (ShortComplex.moduleCatCyclesIso <| normHomCompSub A g).inv ≫
+    ShortComplex.homologyπ _ ≫ (groupHomologyIsoOdd A g hg i hi).inv
 
 lemma groupHomologyπOdd_eq_zero_iff (hg : ∀ x, x ∈ Subgroup.zpowers g)
     (i : ℕ) (hi : Odd i) (x : LinearMap.ker (applyAsHom A g - 𝟙 A).hom.hom) :
@@ -131,7 +131,7 @@ lemma groupHomologyπOdd_eq_iff (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g)
     (A : Rep k G) (i : ℕ) (hi : Odd i) (x y : LinearMap.ker (applyAsHom A g - 𝟙 A).hom.hom) :
     groupHomologyπOdd A g hg i hi x = groupHomologyπOdd A g hg i hi y ↔
       x.1 - y.1 ∈ LinearMap.range A.ρ.norm := by
-  rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff]; rfl
+  rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]
 
 end FiniteCyclicGroup
 end Rep
diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean
diff --git a/Mathlib/RingTheory/WittVector/TeichmullerSeries.lean b/Mathlib/RingTheory/WittVector/TeichmullerSeries.lean
diff --git a/Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean b/Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean
diff --git a/Mathlib/Topology/Algebra/ProperAction/Basic.lean b/Mathlib/Topology/Algebra/ProperAction/Basic.lean
diff --git a/Mathlib/Topology/Convenient/GeneratedBy.lean b/Mathlib/Topology/Convenient/GeneratedBy.lean
