chore: tidy various files (#5233)

Archive/Imo/Imo2011Q5.lean

@@ -43,24 +43,24 @@ theorem imo2011_q5 (f : ℤ → ℤ) (hpos : ∀ n : ℤ, 0 < f n) (hdvd : ∀ m
         _ ≤ f n - f m := (le_of_dvd (sub_pos.mpr h_fm_lt_fn) ?_)
         _ < f n := sub_lt_self _ (hpos m)
       -- ⊢ f (m - n) ∣ f n - f m
-      rw [← dvd_neg, neg_sub];
+      rw [← dvd_neg, neg_sub]
       exact hdvd m n
     have h_d_eq_zero : d = 0 := by
       obtain hd | hd | hd : d > 0 ∨ d = 0 ∨ d < 0 := trichotomous d 0
       · -- d > 0
         have h₁ : f n ≤ d := le_of_dvd hd h_fn_dvd_d
         have h₂ : ¬f n ≤ d := not_le.mpr h_d_lt_fn
         contradiction
-      ·-- d = 0
+      · -- d = 0
         exact hd
       · -- d < 0
         have h₁ : f n ≤ -d := le_of_dvd (neg_pos.mpr hd) h_fn_dvd_d.neg_right
         have h₂ : ¬f n ≤ -d := not_le.mpr h_neg_d_lt_fn
         contradiction
     have h₁ : f m = f (m - n) := sub_eq_zero.mp h_d_eq_zero
     have h₂ : f (m - n) ∣ f m - f n := hdvd m n
-    rw [← h₁] at h₂ 
+    rw [← h₁] at h₂
     exact (dvd_iff_dvd_of_dvd_sub h₂).mp dvd_rfl
-  ·-- m = n
+  · -- m = n
     rw [h_fm_eq_fn]
 #align imo2011_q5 imo2011_q5

Archive/Imo/Imo2019Q4.lean

@@ -41,15 +41,14 @@ namespace Imo2019Q4
 
 theorem upper_bound {k n : ℕ} (hk : k > 0)
     (h : (k ! : ℤ) = ∏ i in range n, ((2:ℤ) ^ n - (2:ℤ) ^ i)) : n < 6 := by
-  have prime_2 : Prime (2 : ℤ) := prime_iff_prime_int.mp prime_two
   have h2 : n * (n - 1) / 2 < k := by
     suffices multiplicity 2 (k ! : ℤ) = (n * (n - 1) / 2 : ℕ) by
       rw [← PartENat.coe_lt_coe, ← this]; change multiplicity ((2 : ℕ) : ℤ) _ < _
       simp_rw [Int.coe_nat_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm]
-    rw [h, multiplicity.Finset.prod prime_2, ← sum_range_id, Nat.cast_sum]
+    rw [h, multiplicity.Finset.prod Int.prime_two, ← sum_range_id, Nat.cast_sum]
     apply sum_congr rfl; intro i hi
-    rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime prime_2]
-    rwa [multiplicity_pow_self_of_prime prime_2, multiplicity_pow_self_of_prime prime_2,
+    rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime Int.prime_two]
+    rwa [multiplicity_pow_self_of_prime Int.prime_two, multiplicity_pow_self_of_prime Int.prime_two,
       PartENat.coe_lt_coe, ← mem_range]
   rw [← not_le]; intro hn
   apply _root_.ne_of_lt _ h.symm

Mathlib/Algebra/Group/Defs.lean

@@ -124,13 +124,13 @@ section Mul
 variable [Mul G]
 
 /-- `leftMul g` denotes left multiplication by `g` -/
-@[to_additive "`left_add g` denotes left addition by `g`"]
+@[to_additive "`leftAdd g` denotes left addition by `g`"]
 def leftMul : G → G → G := fun g : G ↦ fun x : G ↦ g * x
 #align left_mul leftMul
 #align left_add leftAdd
 
 /-- `rightMul g` denotes right multiplication by `g` -/
-@[to_additive "`right_add g` denotes right addition by `g`"]
+@[to_additive "`rightAdd g` denotes right addition by `g`"]
 def rightMul : G → G → G := fun g : G ↦ fun x : G ↦ x * g
 #align right_mul rightMul
 #align right_add rightAdd

Mathlib/Algebra/Lie/OfAssociative.lean

@@ -171,35 +171,35 @@ def toLieHom : A →ₗ⁅R⁆ B :=
 instance : Coe (A →ₐ[R] B) (A →ₗ⁅R⁆ B) :=
   ⟨toLieHom⟩
 
-/-- Porting note: is a syntactic tautology
+/- Porting note: is a syntactic tautology
 @[simp]
 theorem toLieHom_coe : f.toLieHom = ↑f :=
   rfl
-#align alg_hom.to_lie_hom_coe AlgHom.toLieHom_coe
 -/
+#noalign alg_hom.to_lie_hom_coe
 
 @[simp]
-theorem coe_to_lieHom : ((f : A →ₗ⁅R⁆ B) : A → B) = f :=
+theorem coe_toLieHom : ((f : A →ₗ⁅R⁆ B) : A → B) = f :=
   rfl
-#align alg_hom.coe_to_lie_hom AlgHom.coe_to_lieHom
+#align alg_hom.coe_to_lie_hom AlgHom.coe_toLieHom
 
 theorem toLieHom_apply (x : A) : f.toLieHom x = f x :=
   rfl
 #align alg_hom.to_lie_hom_apply AlgHom.toLieHom_apply
 
 @[simp]
-theorem to_lieHom_id : (AlgHom.id R A : A →ₗ⁅R⁆ A) = LieHom.id :=
+theorem toLieHom_id : (AlgHom.id R A : A →ₗ⁅R⁆ A) = LieHom.id :=
   rfl
-#align alg_hom.to_lie_hom_id AlgHom.to_lieHom_id
+#align alg_hom.to_lie_hom_id AlgHom.toLieHom_id
 
 @[simp]
-theorem to_lieHom_comp : (g.comp f : A →ₗ⁅R⁆ C) = (g : B →ₗ⁅R⁆ C).comp (f : A →ₗ⁅R⁆ B) :=
+theorem toLieHom_comp : (g.comp f : A →ₗ⁅R⁆ C) = (g : B →ₗ⁅R⁆ C).comp (f : A →ₗ⁅R⁆ B) :=
   rfl
-#align alg_hom.to_lie_hom_comp AlgHom.to_lieHom_comp
+#align alg_hom.to_lie_hom_comp AlgHom.toLieHom_comp
 
-theorem to_lieHom_injective {f g : A →ₐ[R] B} (h : (f : A →ₗ⁅R⁆ B) = (g : A →ₗ⁅R⁆ B)) : f = g := by
+theorem toLieHom_injective {f g : A →ₐ[R] B} (h : (f : A →ₗ⁅R⁆ B) = (g : A →ₗ⁅R⁆ B)) : f = g := by
   ext a; exact LieHom.congr_fun h a
-#align alg_hom.to_lie_hom_injective AlgHom.to_lieHom_injective
+#align alg_hom.to_lie_hom_injective AlgHom.toLieHom_injective
 
 end AlgHom
 

Mathlib/Algebra/Lie/UniversalEnveloping.lean

@@ -45,7 +45,6 @@ variable (R : Type u₁) (L : Type u₂)
 
 variable [CommRing R] [LieRing L] [LieAlgebra R L]
 
--- mathport name: exprιₜ
 local notation "ιₜ" => TensorAlgebra.ι R
 
 namespace UniversalEnvelopingAlgebra
@@ -68,7 +67,8 @@ def UniversalEnvelopingAlgebra :=
 
 namespace UniversalEnvelopingAlgebra
 
--- Porting note: the next three instances were derived automatically in mathlib3.
+-- Porting note(https://github.com/leanprover-community/mathlib4/issues/5020): the next three
+-- instances were derived automatically in mathlib3.
 
 instance instInhabited : Inhabited (UniversalEnvelopingAlgebra R L) :=
   inferInstanceAs (Inhabited (RingQuot (UniversalEnvelopingAlgebra.Rel R L)))
@@ -97,7 +97,7 @@ def ι : L →ₗ⁅R⁆ UniversalEnvelopingAlgebra R L :=
   { (mkAlgHom R L).toLinearMap.comp ιₜ with
     map_lie' := fun {x y} => by
       suffices mkAlgHom R L (ιₜ ⁅x, y⁆ + ιₜ y * ιₜ x) = mkAlgHom R L (ιₜ x * ιₜ y) by
-        rw [AlgHom.map_mul] at this ; simp [LieRing.of_associative_ring_bracket, ← this]
+        rw [AlgHom.map_mul] at this; simp [LieRing.of_associative_ring_bracket, ← this]
       exact RingQuot.mkAlgHom_rel _ (Rel.lie_compat x y) }
 #align universal_enveloping_algebra.ι UniversalEnvelopingAlgebra.ι
 
@@ -117,10 +117,10 @@ def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A)
     ext
     -- Porting note: was
     -- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
-    --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_to_lieHom,
+    --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_toLieHom,
     --   LieHom.coe_mk, Function.comp_apply, AlgHom.toLinearMap_apply,
     --   RingQuot.liftAlgHom_mkAlgHom_apply]
-    simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_to_lieHom,
+    simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom,
       UniversalEnvelopingAlgebra.ι_apply, mkAlgHom]
     rw [RingQuot.liftAlgHom_mkAlgHom_apply]
     simp only [TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap]
@@ -131,7 +131,7 @@ def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A)
     -- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
     --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_linearMap_comp,
     --   AlgHom.comp_toLinearMap, Function.comp_apply, AlgHom.toLinearMap_apply,
-    --   RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_to_lieHom, LieHom.coe_mk]
+    --   RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_toLieHom, LieHom.coe_mk]
     simp [mkAlgHom]
 #align universal_enveloping_algebra.lift UniversalEnvelopingAlgebra.lift
 

Mathlib/Algebra/NeZero.lean

@@ -52,32 +52,39 @@ section
 variable {α : Type _} [Zero α]
 
 @[simp] lemma zero_ne_one [One α] [NeZero (1 : α)] : (0 : α) ≠ 1 := NeZero.ne' (1 : α)
+#align zero_ne_one zero_ne_one
+
 @[simp] lemma one_ne_zero [One α] [NeZero (1 : α)] : (1 : α) ≠ 0 := NeZero.ne (1 : α)
 #align one_ne_zero one_ne_zero
-#align zero_ne_one zero_ne_one
 
 lemma ne_zero_of_eq_one [One α] [NeZero (1 : α)] {a : α} (h : a = 1) : a ≠ 0 := h ▸ one_ne_zero
 #align ne_zero_of_eq_one ne_zero_of_eq_one
 
 lemma two_ne_zero [OfNat α 2] [NeZero (2 : α)] : (2 : α) ≠ 0 := NeZero.ne (2 : α)
+#align two_ne_zero two_ne_zero
+
 lemma three_ne_zero [OfNat α 3] [NeZero (3 : α)] : (3 : α) ≠ 0 := NeZero.ne (3 : α)
+#align three_ne_zero three_ne_zero
+
 lemma four_ne_zero [OfNat α 4] [NeZero (4 : α)] : (4 : α) ≠ 0 := NeZero.ne (4 : α)
 #align four_ne_zero four_ne_zero
-#align three_ne_zero three_ne_zero
-#align two_ne_zero two_ne_zero
 
 variable (α)
 
 lemma zero_ne_one' [One α] [NeZero (1 : α)] : (0 : α) ≠ 1 := zero_ne_one
+#align zero_ne_one' zero_ne_one'
+
 lemma one_ne_zero' [One α] [NeZero (1 : α)] : (1 : α) ≠ 0 := one_ne_zero
+#align one_ne_zero' one_ne_zero'
+
 lemma two_ne_zero' [OfNat α 2] [NeZero (2 : α)] : (2 : α) ≠ 0 := two_ne_zero
+#align two_ne_zero' two_ne_zero'
+
 lemma three_ne_zero' [OfNat α 3] [NeZero (3 : α)] : (3 : α) ≠ 0 := three_ne_zero
+#align three_ne_zero' three_ne_zero'
+
 lemma four_ne_zero' [OfNat α 4] [NeZero (4 : α)] : (4 : α) ≠ 0 := four_ne_zero
 #align four_ne_zero' four_ne_zero'
-#align three_ne_zero' three_ne_zero'
-#align two_ne_zero' two_ne_zero'
-#align one_ne_zero' one_ne_zero'
-#align zero_ne_one' zero_ne_one'
 
 end
 

Mathlib/Algebra/Order/Monoid/NatCast.lean

@@ -72,29 +72,33 @@ variable [CovariantClass α α (·+·) (·≤·)]
 
 /-- See `zero_lt_two'` for a version with the type explicit. -/
 @[simp] lemma zero_lt_two : (0 : α) < 2 := zero_lt_one.trans_le one_le_two
+#align zero_lt_two zero_lt_two
+
 /-- See `zero_lt_three'` for a version with the type explicit. -/
 @[simp] lemma zero_lt_three : (0 : α) < 3 := by
   rw [← two_add_one_eq_three]
   exact lt_add_of_lt_of_nonneg zero_lt_two zero_le_one
+#align zero_lt_three zero_lt_three
+
 /-- See `zero_lt_four'` for a version with the type explicit. -/
 @[simp] lemma zero_lt_four : (0 : α) < 4 := by
   rw [← three_add_one_eq_four]
   exact lt_add_of_lt_of_nonneg zero_lt_three zero_le_one
 #align zero_lt_four zero_lt_four
-#align zero_lt_three zero_lt_three
-#align zero_lt_two zero_lt_two
 
 variable (α)
 
 /-- See `zero_lt_two` for a version with the type implicit. -/
 lemma zero_lt_two' : (0 : α) < 2 := zero_lt_two
+#align zero_lt_two' zero_lt_two'
+
 /-- See `zero_lt_three` for a version with the type implicit. -/
 lemma zero_lt_three' : (0 : α) < 3 := zero_lt_three
+#align zero_lt_three' zero_lt_three'
+
 /-- See `zero_lt_four` for a version with the type implicit. -/
 lemma zero_lt_four' : (0 : α) < 4 := zero_lt_four
 #align zero_lt_four' zero_lt_four'
-#align zero_lt_three' zero_lt_three'
-#align zero_lt_two' zero_lt_two'
 
 instance ZeroLEOneClass.neZero.two : NeZero (2 : α) := ⟨zero_lt_two.ne'⟩
 instance ZeroLEOneClass.neZero.three : NeZero (3 : α) := ⟨zero_lt_three.ne'⟩
@@ -110,8 +114,10 @@ lemma one_lt_two [CovariantClass α α (·+·) (·<·)] : (1 : α) < 2 := by
 end
 
 alias zero_lt_two ← two_pos
+#align two_pos two_pos
+
 alias zero_lt_three ← three_pos
+#align three_pos three_pos
+
 alias zero_lt_four ← four_pos
 #align four_pos four_pos
-#align three_pos three_pos
-#align two_pos two_pos

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -167,7 +167,7 @@ variable {U : Set 𝕜}
 analytic on a connected set `U` and vanishes in arbitrary neighborhoods of a point `z₀ ∈ U`, then
 it is identically zero in `U`.
 For higher-dimensional versions requiring that the function vanishes in a neighborhood of `z₀`,
-see `eq_on_zero_of_preconnected_of_eventually_eq_zero`. -/
+see `AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero`. -/
 theorem eqOn_zero_of_preconnected_of_frequently_eq_zero (hf : AnalyticOn 𝕜 f U)
     (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfw : ∃ᶠ z in 𝓝[≠] z₀, f z = 0) : EqOn f 0 U :=
   hf.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀
@@ -184,7 +184,7 @@ theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hU
 analytic on a connected set `U` and coincide at points which accumulate to a point `z₀ ∈ U`, then
 they coincide globally in `U`.
 For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
-see `eq_on_of_preconnected_of_eventually_eq`. -/
+see `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`. -/
 theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U)
     (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U := by
   have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 :=
@@ -203,7 +203,7 @@ theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hg : Ana
 field `𝕜` are analytic everywhere and coincide at points which accumulate to a point `z₀`, then
 they coincide globally.
 For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
-see `eq_of_eventually_eq`. -/
+see `AnalyticOn.eq_of_eventuallyEq`. -/
 theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOn 𝕜 f univ) (hg : AnalyticOn 𝕜 g univ)
     (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : f = g :=
   funext fun x =>

Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean

@@ -66,14 +66,14 @@ theorem Complex.hasSum_sin' (z : ℂ) :
     neg_mul, neg_div, mul_assoc, mul_div_cancel_left _ (two_ne_zero : (2 : ℂ) ≠ 0), Complex.div_I]
 #align complex.has_sum_sin' Complex.hasSum_sin'
 
-/-- The power series expansion of `complex.cos`. -/
+/-- The power series expansion of `Complex.cos`. -/
 theorem Complex.hasSum_cos (z : ℂ) :
     HasSum (fun n : ℕ => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (Complex.cos z) := by
   convert Complex.hasSum_cos' z using 1
   simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]
 #align complex.has_sum_cos Complex.hasSum_cos
 
-/-- The power series expansion of `complex.sin`. -/
+/-- The power series expansion of `Complex.sin`. -/
 theorem Complex.hasSum_sin (z : ℂ) :
     HasSum (fun n : ℕ => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (Complex.sin z) := by
   convert Complex.hasSum_sin' z using 1
@@ -101,13 +101,13 @@ theorem Complex.sin_eq_tsum (z : ℂ) :
   (Complex.hasSum_sin z).tsum_eq.symm
 #align complex.sin_eq_tsum Complex.sin_eq_tsum
 
-/-- The power series expansion of `real.cos`. -/
+/-- The power series expansion of `Real.cos`. -/
 theorem Real.hasSum_cos (r : ℝ) :
     HasSum (fun n : ℕ => (-1) ^ n * r ^ (2 * n) / ↑(2 * n)!) (Real.cos r) := by
   exact_mod_cast Complex.hasSum_cos r
 #align real.has_sum_cos Real.hasSum_cos
 
-/-- The power series expansion of `real.sin`. -/
+/-- The power series expansion of `Real.sin`. -/
 theorem Real.hasSum_sin (r : ℝ) :
     HasSum (fun n : ℕ => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1)!) (Real.sin r) := by
   exact_mod_cast Complex.hasSum_sin r

Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

@@ -45,8 +45,8 @@ Given a type `C` with associated `groupoid C` instance.
 
 ## Implementation details
 
-The structure of this file is copied from/inspired by `Mathlib/GroupTheory.Subgroup.Basic`
-and `Mathlib/Combinatorics/SimpleGraph/Subgraph`.
+The structure of this file is copied from/inspired by `Mathlib/GroupTheory/Subgroup/Basic.lean`
+and `Mathlib/Combinatorics/SimpleGraph/Subgraph.lean`.
 
 ## TODO
 
@@ -411,7 +411,7 @@ theorem IsNormal.generatedNormal_le {S : Subgroupoid C} (Sn : S.IsNormal) :
   constructor
   · rintro h c d
     have h' := generated_le_generatedNormal X
-    rw [le_iff] at h h' 
+    rw [le_iff] at h h'
     exact ((subset_generated X c d).trans (@h' c d)).trans (@h c d)
   · rintro h
     apply @sInf_le (Subgroupoid C) _
@@ -538,7 +538,7 @@ theorem mem_map_objs_iff (hφ : Function.Injective φ.obj) (d : D) :
   dsimp [objs, map]
   constructor
   · rintro ⟨f, hf⟩
-    change Map.Arrows φ hφ S d d f at hf ; rw [Map.arrows_iff] at hf 
+    change Map.Arrows φ hφ S d d f at hf ; rw [Map.arrows_iff] at hf
     obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf
     exact ⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩
   · rintro ⟨c, ⟨γ, γS⟩, rfl⟩
@@ -581,13 +581,13 @@ theorem isNormal_map (hφ : Function.Injective φ.obj) (hφ' : im φ hφ = ⊤)
       change Map.Arrows φ hφ S _ _ (𝟙 _); rw [← Functor.map_id]
       constructor; exact Sn.wide c
     conj := fun {d d'} g δ hδ => by
-      rw [mem_map_iff] at hδ 
+      rw [mem_map_iff] at hδ
       obtain ⟨c, c', γ, cd, cd', γS, hγ⟩ := hδ; subst_vars; cases hφ cd'
       have : d' ∈ (im φ hφ).objs := by rw [hφ']; apply mem_top_objs
-      rw [mem_im_objs_iff] at this 
+      rw [mem_im_objs_iff] at this
       obtain ⟨c', rfl⟩ := this
       have : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c') := by rw [hφ']; trivial
-      rw [mem_im_iff] at this 
+      rw [mem_im_iff] at this
       obtain ⟨b, b', f, hb, hb', _, hf⟩ := this; subst_vars; cases hφ hb; cases hφ hb'
       change Map.Arrows φ hφ S (φ.obj c') (φ.obj c') _
       simp only [eqToHom_refl, Category.comp_id, Category.id_comp, inv_eq_inv]
@@ -712,4 +712,3 @@ end Full
 end Subgroupoid
 
 end CategoryTheory
-

Mathlib/Data/Vector3.lean

@@ -282,18 +282,14 @@ theorem vectorAllP_iff_forall (p : α → Prop) (v : Vector3 α n) :
     VectorAllP p v ↔ ∀ i, p (v i) := by
   refine' v.recOn _ _
   · exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩
-  · simp
-    refine' @fun n a v IH =>
+  · simp only [vectorAllP_cons]
+    refine' fun {n} a v IH =>
       (and_congr_right fun _ => IH).trans
         ⟨fun ⟨pa, h⟩ i => by
           refine' i.cases' _ _
           exacts [pa, h], fun h => ⟨_, fun i => _⟩⟩
-    · have h0 := h fz
-      simp at h0
-      exact h0
-    · have hs := h (fs i)
-      simp at hs
-      exact hs
+    · simpa using h fz
+    · simpa using h (fs i)
 #align vector_allp_iff_forall vectorAllP_iff_forall
 
 theorem VectorAllP.imp {p q : α → Prop} (h : ∀ x, p x → q x) {v : Vector3 α n}