chore: tidy various files (#20184)

Ruben-VandeVelde · Ruben-VandeVelde · commit e82091725952 · 2024-12-23T01:07:27.000Z
diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean
@@ -124,9 +124,9 @@ variable (A B : CommRingCat.{u})
 /-- The tensor product `A ⊗[ℤ] B` forms a cocone for `A` and `B`. -/
 @[simps! pt ι]
 def coproductCocone : BinaryCofan A B :=
-BinaryCofan.mk
-  (ofHom (Algebra.TensorProduct.includeLeft (S := ℤ)).toRingHom : A ⟶  of (A ⊗[ℤ] B))
-  (ofHom (Algebra.TensorProduct.includeRight (R := ℤ)).toRingHom : B ⟶  of (A ⊗[ℤ] B))
+  BinaryCofan.mk
+    (ofHom (Algebra.TensorProduct.includeLeft (S := ℤ)).toRingHom : A ⟶  of (A ⊗[ℤ] B))
+    (ofHom (Algebra.TensorProduct.includeRight (R := ℤ)).toRingHom : B ⟶  of (A ⊗[ℤ] B))
 
 @[simp]
 theorem coproductCocone_inl : (coproductCocone A B).inl =
diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean
@@ -711,7 +711,7 @@ end comap
 section NormedLinearOrderedField_comap
 
 variable (K : Type*) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K]
-variable {E : Type*} [NormedAddCommGroup E]  [NormedSpace K E] [FiniteDimensional K E]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
   [ProperSpace E]
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace K F]  [FiniteDimensional K F]
   [ProperSpace F]
diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean
@@ -743,13 +743,9 @@ theorem le_of_forall_sub_le (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a := by
 
 private lemma exists_lt_mul_left_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
     ∃ a' ∈ Set.Ico 0 a, c < a' * b := by
-  rcases eq_or_lt_of_le ha with rfl | ha
-  · rw [zero_mul] at h; exact (not_le_of_lt h hc).rec
-  rcases lt_trichotomy b 0 with hb | rfl | hb
-  · exact (not_le_of_lt (h.trans (mul_neg_of_pos_of_neg ha hb)) hc).rec
-  · rw [mul_zero] at h; exact (not_le_of_lt h hc).rec
-  · obtain ⟨a', ha', a_a'⟩ := exists_between ((div_lt_iff₀ hb).2 h)
-    exact ⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩
+  have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
+  obtain ⟨a', ha', a_a'⟩ := exists_between ((div_lt_iff₀ hb).2 h)
+  exact ⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩
 
 private lemma exists_lt_mul_right_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
     ∃ b' ∈ Set.Ico 0 b, c < a * b' := by
diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -357,7 +357,7 @@ theorem range_fromSpec :
   infer_instance
 
 @[simp]
-theorem opensRange_fromSpec :hU.fromSpec.opensRange = U := Opens.ext (range_fromSpec hU)
+theorem opensRange_fromSpec : hU.fromSpec.opensRange = U := Opens.ext (range_fromSpec hU)
 
 @[reassoc (attr := simp)]
 theorem map_fromSpec {V : X.Opens} (hV : IsAffineOpen V) (f : op U ⟶ op V) :
diff --git a/Mathlib/AlgebraicGeometry/SpreadingOut.lean b/Mathlib/AlgebraicGeometry/SpreadingOut.lean
@@ -60,7 +60,7 @@ lemma injective_germ_basicOpen (U : X.Opens) (hU : IsAffineOpen U)
     (x : X) (hx : x ∈ U) (f : Γ(X, U))
     (hf : x ∈ X.basicOpen f)
     (H : Function.Injective (X.presheaf.germ U x hx)) :
-      Function.Injective (X.presheaf.germ (X.basicOpen f) x hf) := by
+    Function.Injective (X.presheaf.germ (X.basicOpen f) x hf) := by
   rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] at H ⊢
   intros t ht
   have := hU.isLocalization_basicOpen f
@@ -72,13 +72,13 @@ lemma injective_germ_basicOpen (U : X.Opens) (hU : IsAffineOpen U)
 
 lemma Scheme.exists_germ_injective (X : Scheme.{u}) (x : X) [X.IsGermInjectiveAt x] :
     ∃ (U : X.Opens) (hx : x ∈ U),
-        IsAffineOpen U ∧ Function.Injective (X.presheaf.germ U x hx) :=
+      IsAffineOpen U ∧ Function.Injective (X.presheaf.germ U x hx) :=
   Scheme.IsGermInjectiveAt.cond
 
 lemma Scheme.exists_le_and_germ_injective (X : Scheme.{u}) (x : X) [X.IsGermInjectiveAt x]
     (V : X.Opens) (hxV : x ∈ V) :
     ∃ (U : X.Opens) (hx : x ∈ U),
-        IsAffineOpen U ∧ U ≤ V ∧ Function.Injective (X.presheaf.germ U x hx) := by
+      IsAffineOpen U ∧ U ≤ V ∧ Function.Injective (X.presheaf.germ U x hx) := by
   obtain ⟨U, hx, hU, H⟩ := Scheme.IsGermInjectiveAt.cond (x := x)
   obtain ⟨f, hf, hxf⟩ := hU.exists_basicOpen_le ⟨x, hxV⟩ hx
   exact ⟨X.basicOpen f, hxf, hU.basicOpen f, hf, injective_germ_basicOpen U hU x hx f hxf H⟩
@@ -94,7 +94,7 @@ instance (x : X) [X.IsGermInjectiveAt x] [IsOpenImmersion f] :
   simpa
 
 variable {f} in
-lemma isGermInjectiveAt_iff_of_isOpenImmersion {x : X} [IsOpenImmersion f]:
+lemma isGermInjectiveAt_iff_of_isOpenImmersion {x : X} [IsOpenImmersion f] :
     Y.IsGermInjectiveAt (f.base x) ↔ X.IsGermInjectiveAt x := by
   refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
   obtain ⟨U, hxU, hU, hU', H⟩ :=
@@ -126,8 +126,9 @@ lemma Scheme.IsGermInjective.of_openCover
 
 protected
 lemma Scheme.IsGermInjective.Spec
-    (H : ∀ I : Ideal R, I.IsPrime → ∃ f : R, f ∉ I ∧ ∀ (x y : R)
-        (_ : y * x = 0) (_ : y ∉ I), ∃ n, f ^ n * x = 0) : (Spec R).IsGermInjective := by
+    (H : ∀ I : Ideal R, I.IsPrime →
+      ∃ f : R, f ∉ I ∧ ∀ (x y : R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0) :
+    (Spec R).IsGermInjective := by
   refine fun p ↦ ⟨?_⟩
   obtain ⟨f, hf, H⟩ := H p.asIdeal p.2
   refine ⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩
diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
@@ -352,14 +352,16 @@ theorem radius_shift (p : FormalMultilinearSeries 𝕜 E F) : p.shift.radius = p
     intro h
     simp only [le_refl, le_sup_iff, exists_prop, and_true]
     intro n
-    by_cases hr : r = 0
-    · rw [hr]
+    cases eq_zero_or_pos r with
+    | inl hr =>
+      rw [hr]
       cases n <;> simp
-    right
-    replace hr : 0 < (r : ℝ) := pos_iff_ne_zero.mpr hr
-    specialize h (n + 1)
-    rw [le_div_iff₀ hr]
-    rwa [pow_succ, ← mul_assoc] at h
+    | inr hr =>
+      right
+      rw [← NNReal.coe_pos] at hr
+      specialize h (n + 1)
+      rw [le_div_iff₀ hr]
+      rwa [pow_succ, ← mul_assoc] at h
 
 @[simp]
 theorem radius_unshift (p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) :
diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean
@@ -716,8 +716,9 @@ def formalMultilinearSeries_geometric : FormalMultilinearSeries 𝕜 A A :=
 
 /-- The geometric series as an `ofScalars` series. -/
 theorem formalMultilinearSeries_geometric_eq_ofScalars :
-    formalMultilinearSeries_geometric 𝕜 A = FormalMultilinearSeries.ofScalars A fun _ ↦ (1 : 𝕜) :=
-  by simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
+    formalMultilinearSeries_geometric 𝕜 A =
+      FormalMultilinearSeries.ofScalars A fun _ ↦ (1 : 𝕜) := by
+  simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
     formalMultilinearSeries_geometric, one_smul, implies_true]
 
 lemma formalMultilinearSeries_geometric_apply_norm_le (n : ℕ) :
@@ -739,9 +740,9 @@ lemma one_le_formalMultilinearSeries_geometric_radius (𝕜 : Type*) [Nontrivial
 
 lemma formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
     (A : Type*) [NormedRing A] [NormOneClass A] [NormedAlgebra 𝕜 A] :
-    (formalMultilinearSeries_geometric 𝕜 A).radius = 1 := by
-  exact (formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
-    FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto A _ one_ne_zero (by simp))
+    (formalMultilinearSeries_geometric 𝕜 A).radius = 1 :=
+  formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
+    FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto A _ one_ne_zero (by simp)
 
 lemma hasFPowerSeriesOnBall_inverse_one_sub
     (𝕜 : Type*) [NontriviallyNormedField 𝕜]
diff --git a/Mathlib/Analysis/Analytic/OfScalars.lean b/Mathlib/Analysis/Analytic/OfScalars.lean
@@ -164,9 +164,8 @@ private theorem tendsto_succ_norm_div_norm {r r' : ℝ≥0} (hr' : r' ≠ 0)
     (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
       Tendsto (fun n ↦ ‖‖c (n + 1)‖ * r' ^ (n + 1)‖ /
         ‖‖c n‖ * r' ^ n‖) atTop (𝓝 ↑(r' * r)) := by
-  simp_rw [norm_mul, norm_norm, mul_div_mul_comm, ← norm_div, pow_succ,
-    mul_div_right_comm, div_self (pow_ne_zero _ (NNReal.coe_ne_zero.mpr hr')
-    ), one_mul, norm_div, NNReal.norm_eq]
+  simp_rw [norm_mul, norm_norm, mul_div_mul_comm, ← norm_div, pow_succ, mul_div_right_comm,
+    div_self (pow_ne_zero _ (NNReal.coe_ne_zero.mpr hr')), one_mul, norm_div, NNReal.norm_eq]
   exact mul_comm r' r ▸ hc.mul tendsto_const_nhds
 
 theorem ofScalars_radius_ge_inv_of_tendsto {r : ℝ≥0} (hr : r ≠ 0)
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
@@ -159,8 +159,8 @@ instance IsStarNormal.instContinuousFunctionalCalculus {A : Type*} [CStarAlgebra
   spectrum_nonempty a _ := spectrum.nonempty a
   exists_cfc_of_predicate a ha := by
     refine ⟨(StarAlgebra.elemental ℂ a).subtype.comp <| continuousFunctionalCalculus a,
-      ?hom_closedEmbedding, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
-    case hom_closedEmbedding =>
+      ?hom_isClosedEmbedding, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
+    case hom_isClosedEmbedding =>
       exact Isometry.isClosedEmbedding <|
         isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)
     case hom_id => exact congr_arg Subtype.val <| continuousFunctionalCalculus_map_id a
diff --git a/Mathlib/Analysis/Calculus/FirstDerivativeTest.lean b/Mathlib/Analysis/Calculus/FirstDerivativeTest.lean
@@ -46,8 +46,8 @@ lemma isLocalMax_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g
     (h : ContinuousAt f b)
     (hd₀ : DifferentiableOn ℝ f (Ioo a b))
     (hd₁ : DifferentiableOn ℝ f (Ioo b c))
-    (h₀ :  ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
-    (h₁ :  ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsLocalMax f b :=
+    (h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
+    (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsLocalMax f b :=
   have hIoc : ContinuousOn f (Ioc a b) :=
     Ioo_union_right g₀ ▸ hd₀.continuousOn.union_continuousAt (isOpen_Ioo (a := a) (b := b))
       (by simp_all)
@@ -65,20 +65,20 @@ lemma isLocalMin_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ}
     (hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
     (h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
     (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsLocalMin f b := by
-    have := isLocalMax_of_deriv_Ioo (f := -f) g₀ g₁
-      (by simp_all) hd₀.neg hd₁.neg
-      (fun x hx => deriv.neg (f := f) ▸ Left.nonneg_neg_iff.mpr <|h₀ x hx)
-      (fun x hx => deriv.neg (f := f) ▸ Left.neg_nonpos_iff.mpr <|h₁ x hx)
-    exact (neg_neg f) ▸ IsLocalMax.neg this
+  have := isLocalMax_of_deriv_Ioo (f := -f) g₀ g₁
+    (by simp_all) hd₀.neg hd₁.neg
+    (fun x hx => deriv.neg (f := f) ▸ Left.nonneg_neg_iff.mpr <|h₀ x hx)
+    (fun x hx => deriv.neg (f := f) ▸ Left.neg_nonpos_iff.mpr <|h₁ x hx)
+  exact (neg_neg f) ▸ IsLocalMax.neg this
 
  /-- The First-Derivative Test from calculus, maxima version,
  expressed in terms of left and right filters. -/
 lemma isLocalMax_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
     (hd₀ : ∀ᶠ x in 𝓝[<] b, DifferentiableAt ℝ f x) (hd₁ : ∀ᶠ x in 𝓝[>] b, DifferentiableAt ℝ f x)
-    (h₀  : ∀ᶠ x in 𝓝[<] b, 0 ≤ deriv f x) (h₁  : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) :
+    (h₀ : ∀ᶠ x in 𝓝[<] b, 0 ≤ deriv f x) (h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) :
     IsLocalMax f b := by
-  obtain ⟨a,ha⟩ := (nhdsWithin_Iio_basis' ⟨b - 1, sub_one_lt b⟩).eventually_iff.mp <| hd₀.and h₀
-  obtain ⟨c,hc⟩ := (nhdsWithin_Ioi_basis' ⟨b + 1, lt_add_one b⟩).eventually_iff.mp <| hd₁.and h₁
+  obtain ⟨a, ha⟩ := (nhdsWithin_Iio_basis' ⟨b - 1, sub_one_lt b⟩).eventually_iff.mp <| hd₀.and h₀
+  obtain ⟨c, hc⟩ := (nhdsWithin_Ioi_basis' ⟨b + 1, lt_add_one b⟩).eventually_iff.mp <| hd₁.and h₁
   exact isLocalMax_of_deriv_Ioo ha.1 hc.1 h
     (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
     (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
@@ -88,10 +88,10 @@ lemma isLocalMax_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
  expressed in terms of left and right filters. -/
 lemma isLocalMin_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
     (hd₀ : ∀ᶠ x in 𝓝[<] b, DifferentiableAt ℝ f x) (hd₁ : ∀ᶠ x in 𝓝[>] b, DifferentiableAt ℝ f x)
-    (h₀  : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁  : ∀ᶠ x in 𝓝[>] b, deriv f x ≥ 0) :
+    (h₀ : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≥ 0) :
     IsLocalMin f b := by
-  obtain ⟨a,ha⟩ := (nhdsWithin_Iio_basis' ⟨b - 1, sub_one_lt b⟩).eventually_iff.mp <| hd₀.and h₀
-  obtain ⟨c,hc⟩ := (nhdsWithin_Ioi_basis' ⟨b + 1, lt_add_one b⟩).eventually_iff.mp <| hd₁.and h₁
+  obtain ⟨a, ha⟩ := (nhdsWithin_Iio_basis' ⟨b - 1, sub_one_lt b⟩).eventually_iff.mp <| hd₀.and h₀
+  obtain ⟨c, hc⟩ := (nhdsWithin_Ioi_basis' ⟨b + 1, lt_add_one b⟩).eventually_iff.mp <| hd₁.and h₁
   exact isLocalMin_of_deriv_Ioo ha.1 hc.1 h
     (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
     (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
@@ -100,15 +100,15 @@ lemma isLocalMin_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
 /-- The First Derivative test, maximum version. -/
 theorem isLocalMax_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
     (hd : ∀ᶠ x in 𝓝[≠] b, DifferentiableAt ℝ f x)
-    (h₀  : ∀ᶠ x in 𝓝[<] b, 0 ≤ deriv f x) (h₁  : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) :
+    (h₀ : ∀ᶠ x in 𝓝[<] b, 0 ≤ deriv f x) (h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) :
     IsLocalMax f b :=
   isLocalMax_of_deriv' h
     (nhds_left'_le_nhds_ne _ (by tauto)) (nhds_right'_le_nhds_ne _ (by tauto)) h₀ h₁
 
 /-- The First Derivative test, minimum version. -/
 theorem isLocalMin_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
     (hd : ∀ᶠ x in 𝓝[≠] b, DifferentiableAt ℝ f x)
-    (h₀  : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁  : ∀ᶠ x in 𝓝[>] b, 0 ≤ deriv f x) :
+    (h₀ : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁ : ∀ᶠ x in 𝓝[>] b, 0 ≤ deriv f x) :
     IsLocalMin f b :=
   isLocalMin_of_deriv' h
     (nhds_left'_le_nhds_ne _ (by tauto)) (nhds_right'_le_nhds_ne _ (by tauto)) h₀ h₁
diff --git a/Mathlib/CategoryTheory/Comma/Presheaf/Colimit.lean b/Mathlib/CategoryTheory/Comma/Presheaf/Colimit.lean
@@ -22,8 +22,6 @@ open Category Opposite Limits
 universe w v u
 
 variable {C : Type u} [Category.{v} C] {A : Cᵒᵖ ⥤ Type v}
-
-
 variable {J : Type v} [SmallCategory J] {A : Cᵒᵖ ⥤ Type v} (F : J ⥤ Over A)
 
 -- We introduce some local notation to reduce visual noise in the following proof
diff --git a/Mathlib/CategoryTheory/Grothendieck.lean b/Mathlib/CategoryTheory/Grothendieck.lean
@@ -104,15 +104,15 @@ attribute [local simp] eqToHom_map
 instance : Category (Grothendieck F) where
   Hom X Y := Grothendieck.Hom X Y
   id X := Grothendieck.id X
-  comp := @fun _ _ _ f g => Grothendieck.comp f g
-  comp_id := @fun X Y f => by
+  comp f g := Grothendieck.comp f g
+  comp_id {X Y} f := by
     dsimp; ext
     · simp [comp, id]
     · dsimp [comp, id]
       rw [← NatIso.naturality_2 (eqToIso (F.map_id Y.base)) f.fiber]
       simp
-  id_comp := @fun X Y f => by dsimp; ext <;> simp [comp, id]
-  assoc := @fun W X Y Z f g h => by
+  id_comp f := by dsimp; ext <;> simp [comp, id]
+  assoc f g h := by
     dsimp; ext
     · simp [comp, id]
     · dsimp [comp, id]
@@ -160,7 +160,7 @@ variable (F)
 @[simps!]
 def forget : Grothendieck F ⥤ C where
   obj X := X.1
-  map := @fun _ _ f => f.1
+  map f := f.1
 
 end
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk.lean b/Mathlib/Combinatorics/SimpleGraph/Walk.lean
@@ -567,7 +567,7 @@ lemma getVert_eq_support_get? {u v n} (p : G.Walk u v) (h2 : n ≤ p.length) :
     · simp only [hn, getVert_zero, List.length_cons, Nat.zero_lt_succ, List.getElem?_eq_getElem,
       List.getElem_cons_zero]
     · push_neg at hn
-      nth_rewrite 2 [show n = (n - 1) + 1 from by omega]
+      nth_rewrite 2 [← Nat.sub_one_add_one hn]
       rw [Walk.getVert_cons q h hn, List.getElem?_cons_succ]
       exact getVert_eq_support_get? q (Nat.sub_le_of_le_add (Walk.length_cons _ _ ▸ h2))
 
diff --git a/Mathlib/Data/Finset/Max.lean b/Mathlib/Data/Finset/Max.lean
@@ -186,7 +186,7 @@ def max' (s : Finset α) (H : s.Nonempty) : α :=
 variable (s : Finset α) (H : s.Nonempty) {x : α}
 
 theorem min'_mem : s.min' H ∈ s :=
-  mem_of_min <| by simp only [Finset.min, min', id_eq, coe_inf']; rfl
+  mem_of_min <| by simp only [Finset.min, min', id_eq, coe_inf', Function.comp_def]
 
 theorem min'_le (x) (H2 : x ∈ s) : s.min' ⟨x, H2⟩ ≤ x :=
   min_le_of_eq H2 (WithTop.coe_untop _ _).symm
@@ -206,7 +206,7 @@ theorem le_min'_iff {x} : x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y :=
 theorem min'_singleton (a : α) : ({a} : Finset α).min' (singleton_nonempty _) = a := by simp [min']
 
 theorem max'_mem : s.max' H ∈ s :=
-  mem_of_max <| by simp only [max', Finset.max, id_eq, coe_sup']; rfl
+  mem_of_max <| by simp only [max', Finset.max, id_eq, coe_sup', Function.comp_def]
 
 theorem le_max' (x) (H2 : x ∈ s) : x ≤ s.max' ⟨x, H2⟩ :=
   le_max_of_eq H2 (WithBot.coe_unbot _ _).symm
diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean
@@ -238,9 +238,11 @@ lemma nodup_tail_reverse (l : List α) (h : l[0]? = l.getLast?) :
         List.dropLast_cons_of_ne_nil hl, List.tail_cons]
       simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem, getElem_cons_zero,
         Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
-        show l.length ≠ 0 from by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
-      rw [h, show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup from by
-        simp [List.dropLast_eq_take, ← List.drop_length_sub_one], List.nodup_append_comm]
+        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
+      rw [h,
+        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
+          simp [List.dropLast_eq_take, ← List.drop_length_sub_one],
+        List.nodup_append_comm]
       simp [List.getLast_eq_getElem]
 
 theorem Nodup.erase_getElem [DecidableEq α] {l : List α} (hl : l.Nodup)
diff --git a/Mathlib/Data/Real/EReal.lean b/Mathlib/Data/Real/EReal.lean
@@ -1471,9 +1471,9 @@ lemma left_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :
 lemma left_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x)
     (hx_ne_top : x ≠ ⊤) (y z : EReal) :
     x * (y + z) = x * y + x * z := by
-  by_cases hx0 : x = 0
-  · simp [hx0]
-  replace hx0 : 0 < x := hx_nonneg.lt_of_ne' hx0
+  cases hx_nonneg.eq_or_gt with
+  | inl hx0 => simp [hx0]
+  | inr hx0 =>
   lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩
   cases y <;> cases z <;>
     simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul];
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
@@ -1586,16 +1586,12 @@ theorem insert_diff_of_not_mem (s) (h : a ∉ t) : insert a s \ t = insert a (s
   classical
     ext x
     by_cases h' : x ∈ t
-    · have : x ≠ a := by
-        intro H
-        rw [H] at h'
-        exact h h'
-      simp [h, h', this]
+    · simp [h, h', ne_of_mem_of_not_mem h' h]
     · simp [h, h']
 
 theorem insert_diff_self_of_not_mem {a : α} {s : Set α} (h : a ∉ s) : insert a s \ {a} = s := by
   ext x
-  simp [and_iff_left_of_imp fun hx : x ∈ s => show x ≠ a from fun hxa => h <| hxa ▸ hx]
+  simp [and_iff_left_of_imp (ne_of_mem_of_not_mem · h)]
 
 @[simp]
 theorem insert_diff_eq_singleton {a : α} {s : Set α} (h : a ∉ s) : insert a s \ s = {a} := by
diff --git a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
@@ -84,7 +84,7 @@ the maximum of of the cardinality of `R`, the cardinality of a transcendence bas
 `ℵ₀`
 
 For a simpler, but less universe-polymorphic statement, see
-`IsAlgCLosed.cardinal_le_max_transcendence_basis'`  -/
+`IsAlgClosed.cardinal_le_max_transcendence_basis'`  -/
 theorem cardinal_le_max_transcendence_basis (hv : IsTranscendenceBasis R v) :
     Cardinal.lift.{max u w} #K ≤ max (max (Cardinal.lift.{max v w} #R)
       (Cardinal.lift.{max u v} #ι)) ℵ₀ :=
@@ -105,7 +105,7 @@ the maximum of of the cardinality of `R`, the cardinality of a transcendence bas
 `ℵ₀`
 
 A less-universe polymorphic, but simpler statement of
-`IsAlgCLosed.cardinal_le_max_transcendence_basis`  -/
+`IsAlgClosed.cardinal_le_max_transcendence_basis`  -/
 theorem cardinal_le_max_transcendence_basis' (hv : IsTranscendenceBasis R v') :
     #K' ≤ max (max #R #ι') ℵ₀ := by
   simpa using cardinal_le_max_transcendence_basis v' hv
@@ -114,7 +114,7 @@ theorem cardinal_le_max_transcendence_basis' (hv : IsTranscendenceBasis R v') :
 cardinality is the same as that of a transcendence basis.
 
 For a simpler, but less universe-polymorphic statement, see
-`IsAlgCLosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'` -/
+`IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'` -/
 theorem cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt [Nontrivial R]
     (hv : IsTranscendenceBasis R v) (hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K) :
     Cardinal.lift.{w} #K = Cardinal.lift.{v} #ι :=
diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean
diff --git a/Mathlib/LinearAlgebra/RootSystem/Hom.lean b/Mathlib/LinearAlgebra/RootSystem/Hom.lean
diff --git a/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean b/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean
diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean
diff --git a/Mathlib/RingTheory/Radical.lean b/Mathlib/RingTheory/Radical.lean
diff --git a/Mathlib/SetTheory/ZFC/Ordinal.lean b/Mathlib/SetTheory/ZFC/Ordinal.lean
diff --git a/Mathlib/Topology/EMetricSpace/Paracompact.lean b/Mathlib/Topology/EMetricSpace/Paracompact.lean
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
diff --git a/Mathlib/Topology/Order/OrderClosedExtr.lean b/Mathlib/Topology/Order/OrderClosedExtr.lean
