Replace old have/replace/suffices syntax; this is exhaustive.

(The same change is done in mathlib at the moment; let's stay ahead of the curve.)

SphereEversion/Local/AmpleRelation.lean

@@ -84,8 +84,7 @@ theorem slice_of_ker_eq_ker {θ : OneJet E F} {p p' : DualPair E} (hpp' : p.π =
     abel
   ext w
   simp only [slice, mem_setOf_eq, map_sub, vadd_eq_add, mem_vadd_set_iff_neg_vadd_mem, key]
-  have : -(φ p.v - φ p'.v) + w + (φ p.v - φ p'.v) = w
-  abel
+  have : -(φ p.v - φ p'.v) + w + (φ p.v - φ p'.v) = w := by abel
   rw [this]
 
 theorem ample_slice_of_ample_slice {θ : OneJet E F} {p p' : DualPair E} (hpp' : p.π = p'.π)

SphereEversion/Local/AmpleSet.lean

@@ -172,8 +172,7 @@ theorem isPathConnected_compl_zero_of_two_le_dim (hdim : 2 ≤ Module.rank ℝ F
       push_neg at h'
       rw [← Submodule.eq_top_iff'] at h'
       rw [← rank_top ℝ, ← h'] at hdim
-      suffices : (2 : Cardinal) ≤ 1
-      exact not_le_of_lt (by norm_num) this
+      suffices (2 : Cardinal) ≤ 1 from not_le_of_lt (by norm_num) this
       have := hdim.trans (rank_span_le _)
       rwa [Cardinal.mk_singleton] at this
     · exact joinedIn_compl_zero_of_not_mem_span hx h

SphereEversion/Loops/DeltaMollifier.lean

@@ -175,8 +175,7 @@ theorem integral_periodize (f : ℝ → E) {a : ℝ} (hf : support f ⊆ Ioc a (
     cases ht
     cases hn
     have : -(1 : ℝ) < n := by linarith
-    have : -1 < n
-    exact_mod_cast this
+    have : -1 < n := mod_cast this
     have : (n : ℝ) < 1 := by linarith
     norm_cast at this
     linarith

SphereEversion/ToMathlib/Analysis/Calculus/AffineMap.lean

@@ -33,8 +33,8 @@ theorem norm_coe_ball_lt (r : ℝ) (x : ball (0 : F) r) : ‖(x : F)‖ < r := b
 
 theorem mapsTo_homothety_ball (c : F) {r : ℝ} (hr : 0 < r) :
     MapsTo (fun y ↦ homothety c r⁻¹ y -ᵥ c) (ball c r) (ball 0 1) := fun y hy ↦ by
-  replace hy : r⁻¹ * ‖y - c‖ < 1
-  · rw [← mul_lt_mul_left hr, ← mul_assoc, mul_inv_cancel hr.ne.symm, mul_one, one_mul]
+  replace hy : r⁻¹ * ‖y - c‖ < 1 := by
+    rw [← mul_lt_mul_left hr, ← mul_assoc, mul_inv_cancel hr.ne.symm, mul_one, one_mul]
     simpa [dist_eq_norm] using hy
   simp only [homothety_apply, vsub_eq_sub, vadd_eq_add, add_sub_cancel, mem_ball_zero_iff,
     norm_smul, Real.norm_eq_abs, abs_eq_self.2 (inv_pos.mpr hr).le, hy]

SphereEversion/ToMathlib/Analysis/ContDiff.lean

@@ -206,8 +206,8 @@ theorem contDiff_parametric_symm_of_deriv_pos {f : E → ℝ → ℝ} (hf : Cont
   · exact fun x t ↦
       ContinuousLinearEquiv.unitsEquivAut ℝ (Units.mk0 (deriv (f x) t) <| ne_of_gt (hderiv x t))
   · intro x t
-    suffices : partialFDerivSnd ℝ f x t 1 = partialDerivSnd f x t
-    · ext
+    suffices partialFDerivSnd ℝ f x t 1 = partialDerivSnd f x t by
+      ext
       simpa only [RelIso.coe_fn_toEquiv, ContinuousLinearEquiv.coe_coe,
         ContinuousLinearEquiv.unitsEquivAut_apply, Units.val_mk0, one_mul]
     apply partialFDerivSnd_one
@@ -248,9 +248,9 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteS
 from `E` to `E →L[ℝ] E`, is smooth away from 0. -/
 theorem contDiffAt_orthogonalProjection_singleton {v₀ : E} (hv₀ : v₀ ≠ 0) :
     ContDiffAt ℝ ⊤ (fun v : E ↦ (ℝ ∙ v).subtypeL.comp (orthogonalProjection (ℝ ∙ v))) v₀ := by
-  suffices : ContDiffAt ℝ ⊤
-    (fun v : E ↦ (1 / ‖v‖ ^ 2) • .toSpanSingleton ℝ v ∘L InnerProductSpace.toDual ℝ E v) v₀
-  · refine this.congr_of_eventuallyEq (Filter.eventually_of_forall fun v ↦ ?_)
+  suffices ContDiffAt ℝ ⊤
+    (fun v : E ↦ (1 / ‖v‖ ^ 2) • .toSpanSingleton ℝ v ∘L InnerProductSpace.toDual ℝ E v) v₀ by
+    refine this.congr_of_eventuallyEq (Filter.eventually_of_forall fun v ↦ ?_)
     dsimp
     rw [orthogonalProjection_singleton']
     rfl

SphereEversion/ToMathlib/Analysis/Convex/Basic.lean

@@ -166,8 +166,7 @@ theorem ReallyConvex.add_mem (hs : ReallyConvex 𝕜 s) {w₁ w₂ : 𝕜} {z₁
   cases subsingleton_or_nontrivial 𝕜
   · have := Module.subsingleton 𝕜 E
     rwa [Subsingleton.mem_iff_nonempty] at hz₁ ⊢
-  suffices : ∑ b : Bool, cond b w₁ w₂ • cond b z₁ z₂ ∈ s
-  · simpa using this
+  suffices ∑ b : Bool, cond b w₁ w₂ • cond b z₁ z₂ ∈ s by simpa using this
   apply hs.sum_mem <;> simp [*]
 
 theorem ReallyConvex.inter {t : Set E} (hs : ReallyConvex 𝕜 s) (ht : ReallyConvex 𝕜 t) :

SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean

@@ -69,9 +69,8 @@ theorem rot_zero (v : E) : ω.rot (0, v) = ContinuousLinearMap.id ℝ E := by
 
 /-- The map `rot` sends `(1, v)` to a transformation which on `(ℝ ∙ v)ᗮ` acts as the negation. -/
 theorem rot_one (v : E) {w : E} (hw : w ∈ (ℝ ∙ v)ᗮ) : ω.rot (1, v) w = -w := by
-  suffices : (orthogonalProjection (Submodule.span ℝ {v}) w : E) +
-    -(orthogonalProjection (Submodule.span ℝ {v})ᗮ w) = -w
-  · simpa [rot]
+  suffices (orthogonalProjection (Submodule.span ℝ {v}) w : E) +
+    -(orthogonalProjection (Submodule.span ℝ {v})ᗮ w) = -w by simpa [rot]
   simp [orthogonalProjection_eq_self_iff.mpr hw,
         orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hw]
 

SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean

@@ -16,8 +16,8 @@ theorem PartialHomeomorph.exists_contDiff_source_univ_target_subset_ball  :
     let e' := e.toHomeomorph
     rcases Euclidean.nhds_basis_ball.mem_iff.1 (ball_mem_nhds c hr) with ⟨ε, ε₀, hε⟩
     set f := (e'.transPartialHomeomorph (.univBall (e c) ε)).transHomeomorph e'.symm
-    have hf : f.target = Euclidean.ball c ε
-    · rw [transHomeomorph_target, Homeomorph.transPartialHomeomorph_target, univBall_target _ ε₀]
+    have hf : f.target = Euclidean.ball c ε := by
+      rw [transHomeomorph_target, Homeomorph.transPartialHomeomorph_target, univBall_target _ ε₀]
       rfl
     refine ⟨f, ?_, ?_, ?_, fun _ ↦ ?_, ?_⟩
     · exact e.symm.contDiff.comp <| contDiff_univBall.comp e.contDiff

SphereEversion/ToMathlib/Equivariant.lean

@@ -251,7 +251,7 @@ instance : EquivLike EquivariantEquiv ℝ ℝ where
   coe_injective' e₁ e₂ h₁ h₂ := by
     rcases e₁ with ⟨f₁, hf₁⟩
     rcases e₂ with ⟨f₂, hf₂⟩
-    suffices : f₁ = f₂ ; · simpa
+    suffices f₁ = f₂ by simpa
     ext
     change (f₁ : ℝ → ℝ)  = f₂ at h₁
     rw [h₁]

SphereEversion/ToMathlib/ExistsOfConvex.lean

@@ -21,8 +21,8 @@ variable {F : Type*} [AddCommGroup F] [Module ℝ F]
 theorem exists_of_convex {P : (Σ x : M, Germ (𝓝 x) F) → Prop}
     (hP : ∀ x : M, ReallyConvex (smoothGerm I x) {φ | P ⟨x, φ⟩})
     (hP' : ∀ x : M, ∃ f : M → F, ∀ᶠ x' in 𝓝 x, P ⟨x', f⟩) : ∃ f : M → F, ∀ x, P ⟨x, f⟩ := by
-  replace hP' : ∀ x : M, ∃ f : M → F, ∃ U ∈ 𝓝 x, ∀ x' ∈ U, P ⟨x', f⟩
-  · intro x
+  replace hP' : ∀ x : M, ∃ f : M → F, ∃ U ∈ 𝓝 x, ∀ x' ∈ U, P ⟨x', f⟩ := by
+    intro x
     rcases hP' x with ⟨f, hf⟩
     exact ⟨f, {x' | P ⟨x', ↑f⟩}, hf, fun _ ↦ id⟩
   choose φ U hU hφ using hP'

SphereEversion/ToMathlib/LinearAlgebra/Basic.lean

@@ -46,8 +46,7 @@ theorem LinearMap.injective_iff_of_direct_sum (f : M →ₛₗ[σ₁₂] M₂) (
     have hu' : f u ∈ map f p := mem_map_of_mem hu
     have hv' : f (-v) ∈ map f q := mem_map_of_mem (q.neg_mem hv)
     rw [← hx] at hv'
-    have H : f u ∈ map f p ⊓ map f q
-    apply mem_inf.mpr ⟨hu', hv'⟩
+    have H : f u ∈ map f p ⊓ map f q := mem_inf.mpr ⟨hu', hv'⟩
     rw [disjoint_iff_inf_le] at h
     rw [hp u hu (h H), zero_add]
     rw [hp u hu (h H), f.map_zero, f.map_neg, eq_comm, neg_eq_zero] at hx

SphereEversion/ToMathlib/LinearAlgebra/Basis.lean

@@ -27,8 +27,8 @@ theorem Basis.flag_zero {n : ℕ} (b : Basis (Fin n) R M) : b.flag 0 = ⊥ := by
 
 @[simp]
 theorem Basis.flag_last {n : ℕ} (b : Basis (Fin n) R M) : b.flag (Fin.last n) = ⊤ := by
-  have : {j : Fin n | (j : Fin <| n + 1) < Fin.last n} = univ
-  · ext l
+  have : {j : Fin n | (j : Fin <| n + 1) < Fin.last n} = univ := by
+    ext l
     simp [Fin.castSucc_lt_last l]
   simp_rw [Basis.flag, this]
   simp [b.span_eq]

SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean

@@ -8,8 +8,8 @@ variable {𝕜 : Type _} [Field 𝕜] {E : Type _} [AddCommGroup E] [Module 𝕜
 theorem two_le_rank_of_rank_lt_rank [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'] {π : E →ₗ[𝕜] 𝕜}
     (hπ : LinearMap.ker π ≠ ⊤) (h : finrank 𝕜 E < finrank 𝕜 E') (φ : E →ₗ[𝕜] E') :
     2 ≤ Module.rank 𝕜 (E' ⧸ Submodule.map φ (LinearMap.ker π)) := by
-  suffices : 2 ≤ finrank 𝕜 (E' ⧸ π.ker.map φ)
-  · rw [← finrank_eq_rank]
+  suffices 2 ≤ finrank 𝕜 (E' ⧸ π.ker.map φ) by
+    rw [← finrank_eq_rank]
     exact_mod_cast this
   apply le_of_add_le_add_right
   rw [Submodule.finrank_quotient_add_finrank (π.ker.map φ)]
@@ -18,4 +18,3 @@ theorem two_le_rank_of_rank_lt_rank [FiniteDimensional 𝕜 E] [FiniteDimensiona
       finrank 𝕜 (π.ker.map φ) ≤ finrank 𝕜 (LinearMap.ker π) := finrank_map_le φ (LinearMap.ker π)
       _ < finrank 𝕜 E := Submodule.finrank_lt (le_top.lt_of_ne hπ)
   linarith
-

SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean

@@ -134,8 +134,8 @@ theorem continuousAt_parametric_primitive_of_dominated {F : X → ℝ → E} (bo
     apply intervalIntegral.continuousWithinAt_primitive hμb₀
     rw [min_eq_right hb₀.1.le, max_eq_right hb₀.2.le]
     exact bound_integrable.mono_fun' (hF_meas x₀) hx₀
-  · suffices : Tendsto (fun x : X × ℝ ↦ ∫ s in b₀..x.2, F x.1 s - F x₀ s ∂μ) (𝓝 (x₀, b₀)) (𝓝 0)
-    · simpa [ContinuousAt]
+  · suffices Tendsto (fun x : X × ℝ ↦ ∫ s in b₀..x.2, F x.1 s - F x₀ s ∂μ) (𝓝 (x₀, b₀)) (𝓝 0) by
+      simpa [ContinuousAt]
     have : ∀ᶠ p : X × ℝ in 𝓝 (x₀, b₀),
         ‖∫ s in b₀..p.2, F p.1 s - F x₀ s ∂μ‖ ≤ |∫ s in b₀..p.2, 2 * bound s ∂μ| := by
       rw [nhds_prod_eq]
@@ -267,17 +267,16 @@ theorem hasFDerivAt_parametric_primitive_of_lip' (F : H → ℝ → E) (F' : ℝ
     exact (this.mono_set <| ordConnected_Ioo.uIcc_subset hs hu).intervalIntegrable
   constructor
   · apply (bound_int ha hsx₀).mono_fun' hF'_meas _
-    replace h_lipsch :
-      ∀ᵐ t ∂volume.restrict (Ι a (s x₀)),
-        LipschitzOnWith (nnabs (bound t)) (fun x : H ↦ F x t) (ball x₀ ε)
-    exact ae_restrict_of_ae_restrict_of_subset (ordConnected_Ioo.uIoc_subset ha hsx₀) h_lipsch
+    replace h_lipsch : ∀ᵐ t ∂volume.restrict (Ι a (s x₀)),
+        LipschitzOnWith (nnabs (bound t)) (fun x : H ↦ F x t) (ball x₀ ε) :=
+      ae_restrict_of_ae_restrict_of_subset (ordConnected_Ioo.uIoc_subset ha hsx₀) h_lipsch
     filter_upwards [h_lipsch, h_diff]
     intro t ht_lip ht_diff
     rw [show bound t = nnabs (bound t) by simp [bound_nonneg t] ]
     exact ht_diff.le_of_lipschitzOn (ball_mem_nhds x₀ ε_pos) ht_lip
   · have D₁ : HasFDerivAt (fun x ↦ φ x (s x₀)) (∫ t in a..s x₀, F' t) x₀ := by
-      replace hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (volume.restrict (Ι a (s x₀)))
-      exact Eventually.mono (ball_mem_nhds x₀ ε_pos) fun x hx ↦ hF_meas_ball hx ha hsx₀
+      replace hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (volume.restrict (Ι a (s x₀))) :=
+        Eventually.mono (ball_mem_nhds x₀ ε_pos) fun x hx ↦ hF_meas_ball hx ha hsx₀
       replace hF_int : IntervalIntegrable (F x₀) volume a (s x₀) := hF_int_ball x₀ x₀_in ha hsx₀
       exact (hasFDerivAt_integral_of_dominated_loc_of_lip_interval _ ε_pos hF_meas hF_int hF'_meas
         (ae_restrict_of_ae_restrict_of_subset (ordConnected_Ioo.uIoc_subset ha hsx₀) h_lipsch)
@@ -382,8 +381,8 @@ theorem hasFDerivAt_parametric_primitive_of_contDiff' {F : H → ℝ → E} (hF
   have cont_x : ∀ x, Continuous (F x) := fun x ↦ hF.continuous.comp (Continuous.Prod.mk x)
   have int_Icc : ∀ x, IntegrableOn (F x) (Icc a₀ b₀) := fun x ↦
     (cont_x x).continuousOn.integrableOn_Icc
-  have int_Ioo : ∀ x, IntegrableOn (F x) (Ioo a₀ b₀)
-  · exact fun x ↦ (int_Icc x).mono_set Ioo_subset_Icc_self
+  have int_Ioo : ∀ x, IntegrableOn (F x) (Ioo a₀ b₀) := by
+    exact fun x ↦ (int_Icc x).mono_set Ioo_subset_Icc_self
   save
   apply
     hasFDerivAt_parametric_primitive_of_lip' _ _ zero_lt_one ha ht₀

SphereEversion/ToMathlib/Topology/Germ.lean

@@ -124,8 +124,8 @@ theorem Filter.Germ.sliceRight_coe {X Y Z : Type _} [TopologicalSpace X] [Topolo
 
 def Filter.Germ.IsConstant {X Y : Type _} [TopologicalSpace X] {x : X} (P : Germ (𝓝 x) Y) : Prop :=
   P.liftOn (fun f ↦ ∀ᶠ x' in 𝓝 x, f x' = f x) <| by
-    suffices : ∀ f g : X → Y, f =ᶠ[𝓝 x] g → (∀ᶠ x' in 𝓝 x, f x' = f x) → ∀ᶠ x' in 𝓝 x, g x' = g x
-    exact fun f g hfg ↦ propext ⟨fun h ↦ this f g hfg h, fun h ↦ this g f hfg.symm h⟩
+    suffices ∀ f g : X → Y, f =ᶠ[𝓝 x] g → (∀ᶠ x' in 𝓝 x, f x' = f x) → ∀ᶠ x' in 𝓝 x, g x' = g x from
+      fun f g hfg ↦ propext ⟨fun h ↦ this f g hfg h, fun h ↦ this g f hfg.symm h⟩
     rintro f g hfg hf
     refine (hf.and hfg).mono fun x' hx' ↦ ?_
     rw [← hx'.2, hx'.1, hfg.eq_of_nhds]

SphereEversion/ToMathlib/Topology/Paracompact.lean

@@ -21,8 +21,8 @@ theorem exists_countable_locallyFinite_cover {ι X : Type _} [TopologicalSpace X
   have hCU : ∀ n, C n ⊆ U n := fun n x hx ↦
     ⟨K.subset_interior_succ _ hx.1, mt (fun hx₃ ↦ K.subset_interior_succ _ hx₃) hx.2⟩
   have hC : ∀ n, IsCompact (C n) := fun n ↦ (K.isCompact _).diff isOpen_interior
-  have hC' : (⋃ n, C n) = univ
-  · refine Set.univ_subset_iff.mp fun x _ ↦ mem_iUnion.mpr ⟨K'.find x, ?_⟩
+  have hC' : (⋃ n, C n) = univ := by
+    refine Set.univ_subset_iff.mp fun x _ ↦ mem_iUnion.mpr ⟨K'.find x, ?_⟩
     simpa only [K'.find_shiftr] using
       diff_subset_diff_right interior_subset (K'.shiftr.mem_diff_shiftr_find x)
   have hU : ∀ n, IsOpen (U n) := fun n ↦
@@ -35,7 +35,7 @@ theorem exists_countable_locallyFinite_cover {ι X : Type _} [TopologicalSpace X
       exact ⟨this hx₄ hx₁, this hx₂ hx₃⟩
     intro a b ha hb
     by_contra hab
-    replace hab : b + 1 ≤ a; · simpa using hab
+    replace hab : b + 1 ≤ a := by simpa using hab
     exact Set.Nonempty.ne_empty (⟨x, interior_subset hb, ha⟩ : (K b.succ \ K a).Nonempty)
       (Set.diff_eq_empty.mpr (K.subset hab))
   have hU'' : ∀ n x, x ∈ C n → U n ∈ 𝓝 x := fun n x hx ↦