chore: tidy various files (leanprover-community#33687)

Ruben-VandeVelde · Ruben-VandeVelde · commit ee6d0f13b3a2 · 2026-01-08T19:46:02.000Z
diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean
@@ -528,12 +528,11 @@ instance [Nontrivial M] : Nontrivial (LieSubmodule R L M) :=
   (nontrivial_iff R L M).mpr ‹_›
 
 theorem nontrivial_iff_ne_bot {N : LieSubmodule R L M} : Nontrivial N ↔ N ≠ ⊥ := by
-  constructor <;> contrapose!
-  · rintro rfl
-    by_contra!
-      ⟨⟨m₁, h₁ : m₁ ∈ (⊥ : LieSubmodule R L M)⟩, ⟨m₂, h₂ : m₂ ∈ (⊥ : LieSubmodule R L M)⟩, h₁₂⟩
+  constructor
+  · rintro ⟨⟨m₁, h₁⟩, ⟨m₂, h₂⟩, h₁₂⟩ rfl
     simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂
-  · rw [LieSubmodule.eq_bot_iff]
+  · contrapose!
+    rw [LieSubmodule.eq_bot_iff]
     rintro ⟨h⟩ m hm
     simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩
 
diff --git a/Mathlib/Algebra/Module/LocalizedModule/Basic.lean b/Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@@ -63,12 +63,11 @@ lemma oreEqv_eq_r : (OreLocalization.oreEqv S M).r = r S M := by
   · rintro ⟨u, v, h₁, h₂⟩
     use u
     simp only [Submonoid.smul_def, smul_smul, h₂]
-    rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul]
-    rfl
+    rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
   · rintro ⟨u, hu⟩
     use u * a.2, u * b.2
     rw [mul_smul, ← hu, mul_smul, Submonoid.coe_mul, mul_assoc, mul_assoc, mul_comm (a.2 : R)]
-    exact ⟨rfl, rfl⟩
+    simp [Submonoid.smul_def]
 
 theorem r.isEquiv : IsEquiv _ (r S M) :=
   { refl := fun ⟨m, s⟩ => ⟨1, by rw [one_smul]⟩
@@ -371,8 +370,7 @@ theorem mk_cancel_common_right (s s' : S) (m : M) : mk (s' • m) (s * s') = mk
 
 theorem smul'_mk (r : R) (s : S) (m : M) : r • mk m s = mk (r • m) s := by
   refine (OreLocalization.smul_oreDiv _ _ _).trans ?_
-  change (r • 1 : R) • m /ₒ s = _
-  rw [smul_assoc, one_smul]
+  simp
 
 lemma smul_eq_iff_of_mem
     (r : R) (hr : r ∈ S) (x y : LocalizedModule S M) :
@@ -448,11 +446,13 @@ noncomputable instance (priority := 900) algebra' {A : Type*} [Semiring A] [Alge
   algebraMap := numeratorRingHom.comp (algebraMap R A)
   commutes' r x := by
     induction x using induction_on with | _ a s => _
-    change mk _ _ * mk _ _ = mk _ _ * mk _ _
+    simp only [RingHom.coe_comp, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
+      Function.comp_apply]
     rw [mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]
   smul_def' r x := by
     induction x using induction_on with | _ a s => _
-    change _ • mk _ _ = mk _ _ * mk _ _
+    simp only [RingHom.coe_comp, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
+      Function.comp_apply]
     rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]
 
 private lemma example_oreLocalizationInstAlgebra_eq_localizedModuleAlgebra' :
diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean
@@ -243,12 +243,12 @@ lemma odd_sub_one : Odd (a - 1) ↔ Even a :=
   ⟨(by convert ·.add_odd odd_one; rw [sub_add_cancel]), (·.sub_odd odd_one)⟩
 
 @[simp]
-lemma odd_add_two : Odd (a + 2) ↔ Odd a :=
-  by rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]
+lemma odd_add_two : Odd (a + 2) ↔ Odd a := by
+  rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]
 
 @[simp]
-lemma odd_sub_two : Odd (a - 2) ↔ Odd a :=
-  by rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]
+lemma odd_sub_two : Odd (a - 2) ↔ Odd a := by
+  rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]
 
 end Ring
 
diff --git a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean
@@ -103,7 +103,8 @@ lemma sections_smul_localizations_def
     {U : (Opens (PrimeSpectrum.Top R))ᵒᵖ} (x : U.unop)
     (r : (Spec.structureSheaf R).val.obj U)
     (m : Localizations M ↑x) :
-  r • m = (by exact r.1 x : Localization.AtPrime x.1.asIdeal) • m := rfl
+    r • m = (by exact r.1 x : Localization.AtPrime x.1.asIdeal) • m :=
+  rfl
 
 /--
 For any `R`-module `M` and any open subset `U ⊆ Spec R`, `M^~(U)` is an `𝒪_{Spec R}(U)`-submodule
diff --git a/Mathlib/AlgebraicGeometry/Normalization.lean b/Mathlib/AlgebraicGeometry/Normalization.lean
@@ -63,10 +63,10 @@ def normalizationDiagram : Y.Opensᵒᵖ ⥤ CommRingCat where
 
 /-- The inclusion from the structure presheaf of `Y` to the integral closure of `Y` in `X`. -/
 def normalizationDiagramMap : Y.presheaf ⟶ f.normalizationDiagram where
-    app U :=
-      letI := (f.app U.unop).hom.toAlgebra
-      CommRingCat.ofHom (algebraMap Γ(Y, U.unop) (integralClosure Γ(Y, U.unop) Γ(X, f ⁻¹ᵁ U.unop)))
-    naturality {U V} i := by ext x; exact Subtype.ext congr($(f.naturality i) x)
+  app U :=
+    letI := (f.app U.unop).hom.toAlgebra
+    CommRingCat.ofHom (algebraMap Γ(Y, U.unop) (integralClosure Γ(Y, U.unop) Γ(X, f ⁻¹ᵁ U.unop)))
+  naturality {U V} i := by ext x; exact Subtype.ext congr($(f.naturality i) x)
 
 variable [QuasiCompact f] [QuasiSeparated f]
 
diff --git a/Mathlib/AlgebraicTopology/ModelCategory/Bifibrant.lean b/Mathlib/AlgebraicTopology/ModelCategory/Bifibrant.lean
@@ -153,7 +153,7 @@ that are both cofibrant and fibrant.
 `BifibrantObject`. Otherwise, the typeclasses `IsCofibrant` and
 `IsFibrant` are preferred.) -/
 def bifibrantObjects : ObjectProperty C :=
-    cofibrantObjects C ⊓ fibrantObjects C
+  cofibrantObjects C ⊓ fibrantObjects C
 
 variable (C) in
 lemma bifibrantObjects_le_cofibrantObject :
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Norm.lean b/Mathlib/Analysis/Calculus/FDeriv/Norm.lean
@@ -80,11 +80,12 @@ theorem ContDiffAt.contDiffAt_norm_of_smul (h : ContDiffAt ℝ n (‖·‖) (t 
   · apply contDiffAt_zero.2
     exact ⟨univ, univ_mem, continuous_norm.continuousOn⟩
   obtain rfl | ht := eq_or_ne t 0
-  · by_cases! hE : Nontrivial E
-    · rw [zero_smul] at h
-      exact (mt (ContDiffAt.differentiableAt · hn)) (not_differentiableAt_norm_zero E) h |>.elim
-    · rw [eq_const_of_subsingleton (‖·‖) 0]
+  · suffices Subsingleton E by
+      rw [eq_const_of_subsingleton (‖·‖) 0]
       exact contDiffAt_const
+    rw [zero_smul] at h
+    by_contra!
+    exact not_differentiableAt_norm_zero E <| h.differentiableAt hn
   · exact contDiffAt_norm_smul_iff ht |>.2 h
 
 theorem HasStrictFDerivAt.hasStrictFDerivAt_norm_smul
@@ -146,10 +147,10 @@ theorem differentiableAt_norm_smul (ht : t ≠ 0) :
 theorem DifferentiableAt.differentiableAt_norm_of_smul (h : DifferentiableAt ℝ (‖·‖) (t • x)) :
     DifferentiableAt ℝ (‖·‖) x := by
   obtain rfl | ht := eq_or_ne t 0
-  · by_cases! hE : Nontrivial E
-    · rw [zero_smul] at h
-      exact not_differentiableAt_norm_zero E h |>.elim
-    · exact (hasFDerivAt_of_subsingleton _ _).differentiableAt
+  · suffices Subsingleton E from (hasFDerivAt_of_subsingleton _ _).differentiableAt
+    rw [zero_smul] at h
+    by_contra!
+    exact not_differentiableAt_norm_zero E h
   · exact differentiableAt_norm_smul ht |>.2 h
 
 theorem DifferentiableAt.fderiv_norm_self {x : E} (h : DifferentiableAt ℝ (‖·‖) x) :
diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
@@ -64,9 +64,7 @@ instance : LocPathConnectedSpace ℍ := isOpenEmbedding_coe.locPathConnectedSpac
 instance : NoncompactSpace ℍ := by
   refine ⟨fun h => ?_⟩
   have : IsCompact (Complex.im ⁻¹' Ioi 0) := isCompact_iff_isCompact_univ.2 h
-  replace := this.isClosed.closure_eq
-  rw [closure_preimage_im, closure_Ioi, Set.ext_iff] at this
-  exact absurd ((this 0).1 (@self_mem_Ici ℝ _ 0)) (@lt_irrefl ℝ _ 0)
+  simpa [closure_preimage_im] using congr(0 ∈ $this.isClosed.closure_eq)
 
 instance : LocallyCompactSpace ℍ :=
   isOpenEmbedding_coe.locallyCompactSpace
diff --git a/Mathlib/Analysis/Distribution/TemperedDistribution.lean b/Mathlib/Analysis/Distribution/TemperedDistribution.lean
@@ -94,7 +94,7 @@ set_option backward.privateInPublic true in
 /-- A function of temperate growth `f` defines a tempered distribution via integration, namely
 `g ↦ ∫ (x : E), g x • f x ∂μ`. -/
 def toTemperedDistribution {f : E → F} (hf : f.HasTemperateGrowth) : 𝓢'(E, F) :=
-    toPointwiseConvergenceCLM _ _ _ _ ((integralCLM ℂ μ) ∘L (bilinLeftCLM (lsmul ℂ ℂ) hf))
+  toPointwiseConvergenceCLM _ _ _ _ ((integralCLM ℂ μ) ∘L (bilinLeftCLM (lsmul ℂ ℂ) hf))
 
 set_option backward.privateInPublic true in
 @[simp]
diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean
@@ -131,7 +131,7 @@ lemma Metric.diam_closedBall_eq (x : E) {r : ℝ} (hr : 0 ≤ r) : diam (closedB
     diam_sphere_eq x hr |>.symm.le.trans <| diam_mono sphere_subset_closedBall isBounded_closedBall
 
 lemma Metric.diam_ball_eq (x : E) {r : ℝ} (hr : 0 ≤ r) : diam (ball x r) = 2 * r := by
-    /- This proof could be simplified with `Metric.diam_closure` and `closure_ball`,
+  /- This proof could be simplified with `Metric.diam_closure` and `closure_ball`,
   but we opt for this proof to minimize dependencies. -/
   refine le_antisymm (diam_ball hr) <|
     mul_le_of_forall_lt_of_nonneg (by positivity) diam_nonneg fun a ha ha' r' hr' hr'' ↦ ?_
diff --git a/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean b/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean
@@ -60,8 +60,10 @@ public theorem ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv
   obtain ⟨u, hu⟩ := exists_ne (0 : V)
   obtain ⟨v, huv⟩ := SeparatingDual.exists_ne_zero (R := 𝕜) hu
   obtain ⟨z, hz⟩ : ∃ z : W, ¬ f (smulRight v u) z = (0 : W →L[𝕜] W) z := by
-    rw [← not_forall, ← ContinuousLinearMap.ext_iff, map_eq_zero_iff, ContinuousLinearMap.ext_iff]
-    exact not_forall.mpr ⟨u, huv.isUnit.smul_eq_zero.not.mpr hu⟩
+    simp_rw [← not_forall, ← ContinuousLinearMap.ext_iff, map_eq_zero_iff,
+      ContinuousLinearMap.ext_iff, not_forall, smulRight_apply, zero_apply,
+      smul_eq_zero_iff_left hu]
+    exact ⟨u, huv⟩
   set T := apply' _ (.id 𝕜) z ∘L f.toContinuousAlgHom.toContinuousLinearMap ∘L smulRightL 𝕜 _ _ v
   have hT x : T x = f (smulRight v x) z := rfl
   have this A x : T (A x) = f A (T x) := by
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
@@ -840,17 +840,16 @@ lemma sign_two_zsmul_eq_neg_sign_iff {θ : Angle} :
   rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_neg_sign_iff]
 
 theorem eq_add_pi_of_two_zsmul_eq_of_sign_eq_neg (a b : Real.Angle) (h : (2 : ℤ) • a = (2 : ℤ) • b)
-  (h_sign : a.sign = -b.sign) (h_ne : b.sign ≠ 0) : a = b + π := by
+    (h_sign : a.sign = -b.sign) (h_ne : b.sign ≠ 0) : a = b + π := by
   have h1 := Real.Angle.two_zsmul_eq_iff.mp h
-  rcases h1 with h2 | h3
-  · rw [h2] at h_sign
-    simp only [SignType.self_eq_neg_iff] at h_sign
-    rw [h_sign] at h_ne
-    contradiction
-  · rw [h3]
+  refine h1.resolve_left ?_
+  rintro rfl
+  simp only [SignType.self_eq_neg_iff] at h_sign
+  rw [h_sign] at h_ne
+  contradiction
 
 theorem sub_ne_pi_of_sign_eq_of_sign_ne_zero (a b : Real.Angle) (h_sign : a.sign = b.sign)
-  (h_ne : b.sign ≠ 0) : a - b ≠ π := by
+    (h_ne : b.sign ≠ 0) : a - b ≠ π := by
   intro h
   have h' : a = b + π := by
     simp [← h]
diff --git a/Mathlib/CategoryTheory/Filtered/Basic.lean b/Mathlib/CategoryTheory/Filtered/Basic.lean
@@ -24,7 +24,7 @@ if `C` is a filtered category, there exists a final functor `α ⥤ C` from
 a nonempty directed type (`IsFiltered.isDirected`).
 
 Filtered colimits are often better behaved than arbitrary colimits.
-See `CategoryTheory/Limits/Types` for some details.
+See `Mathlib/CategoryTheory/Limits/Types/` for some details.
 
 Filtered categories are nice because colimits indexed by filtered categories tend to be
 easier to describe than general colimits (and more often preserved by functors).
@@ -49,12 +49,12 @@ All of the above API, except for the `bowtie` and the `tulip`, is also provided
 categories.
 
 ## See also
-In `CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit` we show that filtered colimits
-commute with finite limits.
+In `Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean` we show that filtered
+colimits commute with finite limits.
 
 There is another characterization of filtered categories, namely that whenever `F : J ⥤ C` is a
 functor from a finite category, there is `X : C` such that `Nonempty (limit (F.op ⋙ yoneda.obj X))`.
-This is shown in `CategoryTheory.Limits.Filtered`.
+This is shown in `Mathlib/CategoryTheory/Limits/Filtered.lean`.
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean b/Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean
@@ -11,9 +11,9 @@ public import Mathlib.CategoryTheory.Filtered.Basic
 /-!
 # Preservation of filtered colimits and cofiltered limits.
 Typically forgetful functors from algebraic categories preserve filtered colimits
-(although not general colimits). See e.g. `Algebra/Category/MonCat/FilteredColimits`.
+(although not general colimits). See e.g. `Mathlib/Algebra/Category/MonCat/FilteredColimits.lean`.
 
-Note also that using the results in the file `CategoryTheory.Presentable.Directed`,
+Note also that using the results in the file `Mathlib/CategoryTheory/Presentable/Directed.lean`,
 in order to show that a functor preserves filtered colimits, it would be
 sufficient to check that it preserves colimits indexed by nonempty directed
 types.
diff --git a/Mathlib/CategoryTheory/Pi/Monoidal.lean b/Mathlib/CategoryTheory/Pi/Monoidal.lean
@@ -44,7 +44,7 @@ instance monoidalCategoryStruct : MonoidalCategoryStruct (∀ i, C i) where
 
 @[simp]
 theorem associator_hom_apply {X Y Z : ∀ i, C i} {i : I} :
-  (α_ X Y Z).hom i = (α_ (X i) (Y i) (Z i)).hom := rfl
+    (α_ X Y Z).hom i = (α_ (X i) (Y i) (Z i)).hom := rfl
 
 @[simp]
 theorem associator_inv_apply {X Y Z : ∀ i, C i} {i : I} :
diff --git a/Mathlib/CategoryTheory/Sites/Canonical.lean b/Mathlib/CategoryTheory/Sites/Canonical.lean
@@ -293,10 +293,10 @@ def fullyFaithfulUliftYoneda : (GrothendieckTopology.uliftYoneda.{w} J).FullyFai
   J.yonedaFullyFaithful.comp (fullyFaithfulSheafCompose J fullyFaithfulULiftFunctor)
 
 instance : (GrothendieckTopology.uliftYoneda.{w} J).Full :=
-    (J.fullyFaithfulUliftYoneda).full
+  (J.fullyFaithfulUliftYoneda).full
 
 instance : (GrothendieckTopology.uliftYoneda.{w} J).Faithful :=
-    (J.fullyFaithfulUliftYoneda).faithful
+  (J.fullyFaithfulUliftYoneda).faithful
 
 end GrothendieckTopology
 
diff --git a/Mathlib/CategoryTheory/Sites/Descent/IsStack.lean b/Mathlib/CategoryTheory/Sites/Descent/IsStack.lean
@@ -11,9 +11,9 @@ public import Mathlib.CategoryTheory.Sites.Descent.DescentData
 # Stacks: effectiveness of descent
 
 Let `C` be a category with a Grothendieck topology `J` and `F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat`.
-In this file, we define the typeclass `F.IsStack J` saying that `F` is a stack
-for `J`. (See the terminological note in the file `Sites.Descent.IsPrestack`: we
-do not require that the categories `F.obj (.mk (op S))` are groupoids.)
+In this file, we define the typeclass `F.IsStack J` saying that `F` is a stack for `J`.
+(See the terminological note in the file `Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean`:
+we do not require that the categories `F.obj (.mk (op S))` are groupoids.)
 
 The typeclass `IsStack` extends `IsPrestack`. The effectiveness of descent that
 is required for stacks is expressed by saying that the functors `toDescentData`
@@ -43,7 +43,8 @@ variable {C : Type u} [Category.{v} C]
 
 /-- The property that a pseudofunctor `F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat`
 has effective descent for a Grothendieck topology, i.e. is a stack.
-(See the terminological note in the introduction of the file `Sites.Descent.IsPrestack`.) -/
+(See the terminological note in the introduction of the file
+`Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean`.) -/
 @[stacks 026F]
 class IsStack (F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat.{v', u'}) (J : GrothendieckTopology C) : Prop
     extends F.IsPrestack J where
diff --git a/Mathlib/Geometry/Euclidean/Incenter.lean b/Mathlib/Geometry/Euclidean/Incenter.lean
@@ -115,8 +115,7 @@ lemma excenterWeights_reindex (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset
     (s.reindex e).excenterWeights signs =
       s.excenterWeights (signs.map e.symm) ∘ e.symm := by
   simp_rw [excenterWeights, excenterWeightsUnnorm_reindex, Finset.sum_comp_equiv,
-    Finset.map_univ_equiv]
-  rfl
+    Finset.map_univ_equiv, Pi.smul_comp]
 
 variable {s} in
 lemma ExcenterExists.excenterWeights_ne_zero {signs : Finset (Fin (n + 1))}
diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
@@ -487,7 +487,6 @@ theorem range_mfderiv_coe_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : s
   simp only [fderivWithin_univ, mfld_simps]
   let U := (OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ) n
     (ne_zero_of_mem_unit_sphere (-v))).repr
-  -- Porting note: this `suffices` was a `change`
   suffices
       (fderiv ℝ ((stereoInvFunAux (-v : E) ∘ (↑)) ∘ U.symm) 0).range = (ℝ ∙ (v : E))ᗮ by
     convert this using 4
diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -118,7 +118,7 @@ variable [Group α] [Group G] [Group G']
 @[to_additive /-- A non-cyclic additive group is non-trivial. -/]
 theorem Nontrivial.of_not_isCyclic (nc : ¬IsCyclic α) : Nontrivial α := by
   contrapose! nc
-  exact @isCyclic_of_subsingleton _ _ nc
+  exact isCyclic_of_subsingleton
 
 @[to_additive]
 theorem MonoidHom.map_cyclic [h : IsCyclic G] (σ : G →* G) :
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
@@ -160,7 +160,7 @@ noncomputable def quotTensorEquivQuotSMul (I : Ideal R) :
   (Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) <| by
     rw [← LinearMap.range_comp, ← (Submodule.topEquiv.lTensor I).range_comp, Submodule.smul_eq_map₂,
       map₂_eq_range_lift_comp_mapIncl]
-    exact congr_arg _ (TensorProduct.ext' fun _ _ ↦ rfl))
+    exact congr_arg _ (TensorProduct.ext' fun _ _ ↦ by simp))
 
 variable (M) in
 /-- Right tensoring a module with a quotient of the ring is the same as
diff --git a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean
@@ -70,7 +70,7 @@ variable {E : Type*} [NormedAddCommGroup E]
 
 noncomputable section
 
-open scoped Real NNReal Interval Pointwise Topology BigOperators
+open scoped Real NNReal Interval Pointwise Topology
 
 open Complex MeasureTheory TopologicalSpace Metric Function Set Filter Asymptotics
 
diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean
@@ -17,7 +17,7 @@ public import Mathlib.Topology.MetricSpace.MetricSeparated
 In this file we define the `d`-dimensional Hausdorff measure on an (extended) metric space `X` and
 the Hausdorff dimension of a set in an (extended) metric space. Let `μ d δ` be the maximal outer
 measure such that `μ d δ s ≤ (ediam s) ^ d` for every set of diameter less than `δ`. Then
-the Hausdorff measure `μH[d] s` of `s` is defined as `⨆ δ > 0, μ d δ s`. By Carathéodory theorem
+the Hausdorff measure `μH[d] s` of `s` is defined as `⨆ δ > 0, μ d δ s`. By Carathéodory's theorem
 `MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory`, this is a Borel measure on `X`.
 
 The value of `μH[d]`, `d > 0`, on a set `s` (measurable or not) is given by
@@ -40,7 +40,7 @@ applied to `MeasureTheory.extend m`.
 
 We also define a predicate `MeasureTheory.OuterMeasure.IsMetric` which says that an outer measure
 is additive on metric separated pairs of sets: `μ (s ∪ t) = μ s + μ t` provided that
-`⨅ (x ∈ s) (y ∈ t), edist x y ≠ 0`. This is the property required for the Carathéodory theorem
+`⨅ (x ∈ s) (y ∈ t), edist x y ≠ 0`. This is the property required for Carathéodory's theorem
 `MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory`, so we prove this theorem for any
 metric outer measure, then prove that outer measures constructed using `mkMetric'` are metric outer
 measures.
@@ -126,7 +126,7 @@ namespace OuterMeasure
 /-!
 ### Metric outer measures
 
-In this section we define metric outer measures and prove Carathéodory theorem: a metric outer
+In this section we define metric outer measures and prove Carathéodory's theorem: a metric outer
 measure has the Carathéodory property.
 -/
 
@@ -154,8 +154,8 @@ theorem finset_iUnion_of_pairwise_separated (hm : IsMetric μ) {I : Finset ι} {
       Metric.AreSeparated.finset_iUnion_right fun j hj =>
         hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]
 
-/-- Carathéodory theorem. If `m` is a metric outer measure, then every Borel measurable set `t` is
-Carathéodory measurable: for any (not necessarily measurable) set `s` we have
+/-- **Carathéodory's theorem**. If `m` is a metric outer measure, then every Borel measurable set
+`t` is Carathéodory measurable: for any (not necessarily measurable) set `s` we have
 `μ (s ∩ t) + μ (s \ t) = μ s`. -/
 theorem borel_le_caratheodory (hm : IsMetric μ) : borel X ≤ μ.caratheodory := by
   rw [borel_eq_generateFrom_isClosed]
diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
@@ -124,8 +124,9 @@ unit disk is a root of unity. -/
 theorem pow_eq_one_of_norm_le_one {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
     (hx : ∀ φ : K →+* A, ‖φ x‖ ≤ 1) : ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1 := by
   obtain ⟨a, -, b, -, habne, h⟩ :=
-    @Set.Infinite.exists_ne_map_eq_of_mapsTo _ _ _ _ (x ^ · : ℕ → K) Set.infinite_univ
-      (by exact fun a _ => ⟨hxi.pow a, fun φ => by simp [pow_le_one₀ (norm_nonneg (φ x)) <| hx φ]⟩)
+    Set.Infinite.exists_ne_map_eq_of_mapsTo (f := (x ^ · : ℕ → K)) Set.infinite_univ
+      (fun a _ => mem_setOf.mpr <|
+        ⟨hxi.pow a, fun φ => by simp [pow_le_one₀ (norm_nonneg (φ x)) <| hx φ]⟩)
       (finite_of_norm_le K A (1 : ℝ))
   wlog hlt : b < a
   · exact this K A hx₀ hxi hx b a habne.symm h.symm (habne.lt_or_gt.resolve_right hlt)
diff --git a/Mathlib/Order/CompleteLattice/PiLex.lean b/Mathlib/Order/CompleteLattice/PiLex.lean
@@ -37,9 +37,7 @@ instance : InfSet (Πₗ i, α i) where
 
 theorem sInf_apply (s : Set (Πₗ i, α i)) (i : ι) :
     sInf s i = ⨅ e : {e ∈ s | ∀ j < i, e j = sInf s j}, e.1 i := by
-  dsimp [sInf]
-  rw [inf]
-  rfl
+  simp [sInf, inf]
 
 theorem sInf_apply_le {s : Set (Πₗ i, α i)} {i : ι} {e : Πₗ i, α i}
     (he : e ∈ s) (h : ∀ j < i, e j = sInf s j) : sInf s i ≤ e i := by
diff --git a/Mathlib/RingTheory/DedekindDomain/GaussLemma.lean b/Mathlib/RingTheory/DedekindDomain/GaussLemma.lean
diff --git a/Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean b/Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean
diff --git a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean
diff --git a/Mathlib/Topology/MetricSpace/Similarity.lean b/Mathlib/Topology/MetricSpace/Similarity.lean
diff --git a/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean b/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean
