chore: avoid lean3 style have/suffices (#6964)

Many proofs use the "stream of consciousness" style from Lean 3, rather than `have ... := ` or `suffices ... from/by`.

This PR updates a fraction of these to the preferred Lean 4 style.

I think a good goal would be to delete the "deferred" versions of `have`, `suffices`, and `let` at the bottom of `Mathlib.Tactic.Have`

(Anyone who would like to contribute more cleanup is welcome to push directly to this branch.)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -532,8 +532,8 @@ theorem exists_dvd_and_dvd_of_dvd_mul [GCDMonoid α] {m n k : α} (H : k ∣ m *
     simp
   · obtain ⟨a, ha⟩ := gcd_dvd_left k m
     refine' ⟨gcd k m, a, gcd_dvd_right _ _, _, ha⟩
-    suffices h : gcd k m * a ∣ gcd k m * n
-    · cases' h with b hb
+    suffices h : gcd k m * a ∣ gcd k m * n by
+      cases' h with b hb
       use b
       rw [mul_assoc] at hb
       apply mul_left_cancel₀ h0 hb

Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

@@ -117,20 +117,20 @@ instance : Epi (Abelian.factorThruImage f) :=
   let h := hu.g
   -- By hypothesis, p factors through the kernel of g via some t.
   obtain ⟨t, ht⟩ := kernel.lift' g p hpg
-  have fh : f ≫ h = 0
-  calc
-    f ≫ h = (p ≫ i) ≫ h := (Abelian.image.fac f).symm ▸ rfl
-    _ = ((t ≫ kernel.ι g) ≫ i) ≫ h := (ht ▸ rfl)
-    _ = t ≫ u ≫ h := by simp only [Category.assoc]
-    _ = t ≫ 0 := (hu.w ▸ rfl)
-    _ = 0 := HasZeroMorphisms.comp_zero _ _
+  have fh : f ≫ h = 0 :=
+    calc
+      f ≫ h = (p ≫ i) ≫ h := (Abelian.image.fac f).symm ▸ rfl
+      _ = ((t ≫ kernel.ι g) ≫ i) ≫ h := (ht ▸ rfl)
+      _ = t ≫ u ≫ h := by simp only [Category.assoc]
+      _ = t ≫ 0 := (hu.w ▸ rfl)
+      _ = 0 := HasZeroMorphisms.comp_zero _ _
   -- h factors through the cokernel of f via some l.
   obtain ⟨l, hl⟩ := cokernel.desc' f h fh
-  have hih : i ≫ h = 0
-  calc
-    i ≫ h = i ≫ cokernel.π f ≫ l := hl ▸ rfl
-    _ = 0 ≫ l := by rw [← Category.assoc, kernel.condition]
-    _ = 0 := zero_comp
+  have hih : i ≫ h = 0 :=
+    calc
+      i ≫ h = i ≫ cokernel.π f ≫ l := hl ▸ rfl
+      _ = 0 ≫ l := by rw [← Category.assoc, kernel.condition]
+      _ = 0 := zero_comp
   -- i factors through u = ker h via some s.
   obtain ⟨s, hs⟩ := NormalMono.lift' u i hih
   have hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i := by rw [Category.assoc, hs, Category.id_comp]
@@ -155,20 +155,20 @@ instance : Mono (Abelian.factorThruCoimage f) :=
     let h := hu.g
     -- By hypothesis, i factors through the cokernel of g via some t.
     obtain ⟨t, ht⟩ := cokernel.desc' g i hgi
-    have hf : h ≫ f = 0
-    calc
-      h ≫ f = h ≫ p ≫ i := (Abelian.coimage.fac f).symm ▸ rfl
-      _ = h ≫ p ≫ cokernel.π g ≫ t := (ht ▸ rfl)
-      _ = h ≫ u ≫ t := by simp only [Category.assoc]
-      _ = 0 ≫ t := by rw [← Category.assoc, hu.w]
-      _ = 0 := zero_comp
+    have hf : h ≫ f = 0 :=
+      calc
+        h ≫ f = h ≫ p ≫ i := (Abelian.coimage.fac f).symm ▸ rfl
+        _ = h ≫ p ≫ cokernel.π g ≫ t := (ht ▸ rfl)
+        _ = h ≫ u ≫ t := by simp only [Category.assoc]
+        _ = 0 ≫ t := by rw [← Category.assoc, hu.w]
+        _ = 0 := zero_comp
     -- h factors through the kernel of f via some l.
     obtain ⟨l, hl⟩ := kernel.lift' f h hf
-    have hhp : h ≫ p = 0
-    calc
-      h ≫ p = (l ≫ kernel.ι f) ≫ p := hl ▸ rfl
-      _ = l ≫ 0 := by rw [Category.assoc, cokernel.condition]
-      _ = 0 := comp_zero
+    have hhp : h ≫ p = 0 :=
+      calc
+        h ≫ p = (l ≫ kernel.ι f) ≫ p := hl ▸ rfl
+        _ = l ≫ 0 := by rw [Category.assoc, cokernel.condition]
+        _ = 0 := comp_zero
     -- p factors through u = coker h via some s.
     obtain ⟨s, hs⟩ := NormalEpi.desc' u p hhp
     have hs' : p ≫ cokernel.π g ≫ s = p ≫ 𝟙 I := by rw [← Category.assoc, hs, Category.comp_id]
@@ -304,8 +304,7 @@ theorem σ_comp {X Y : C} (f : X ⟶ Y) : σ ≫ f = Limits.prod.map f f ≫ σ
   obtain ⟨g, hg⟩ :=
     CokernelCofork.IsColimit.desc' isColimitσ (Limits.prod.map f f ≫ σ) (by
       rw [prod.diag_map_assoc, diag_σ, comp_zero])
-  suffices hfg : f = g
-  · rw [← hg, Cofork.π_ofπ, hfg]
+  suffices hfg : f = g by rw [← hg, Cofork.π_ofπ, hfg]
   calc
     f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
     _ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]

Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

@@ -212,9 +212,9 @@ def Adjunction.restrictFullyFaithful (iC : C ⥤ C') (iD : D ⥤ D') {L' : C' 
         simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm
       homEquiv_naturality_right := fun {X Y' Y} f g => by
         apply iC.map_injective
-        suffices : R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)
-        · simp [Trans.trans, this]
-        · apply comm2.hom.naturality g }
+        suffices R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g) by
+          simp [Trans.trans, this]
+        apply comm2.hom.naturality g }
 #align category_theory.adjunction.restrict_fully_faithful CategoryTheory.Adjunction.restrictFullyFaithful
 
 end CategoryTheory

Mathlib/CategoryTheory/Closed/Cartesian.lean

@@ -318,9 +318,9 @@ def zeroMul {I : C} (t : IsInitial I) : A ⨯ I ≅ I where
   hom := Limits.prod.snd
   inv := t.to _
   hom_inv_id := by
-    have : (prod.snd : A ⨯ I ⟶ I) = CartesianClosed.uncurry (t.to _)
-    rw [← curry_eq_iff]
-    apply t.hom_ext
+    have : (prod.snd : A ⨯ I ⟶ I) = CartesianClosed.uncurry (t.to _) := by
+      rw [← curry_eq_iff]
+      apply t.hom_ext
     rw [this, ← uncurry_natural_right, ← eq_curry_iff]
     apply t.hom_ext
   inv_hom_id := t.hom_ext _ _
@@ -407,15 +407,17 @@ def cartesianClosedOfEquiv (e : C ≌ D) [h : CartesianClosed C] : CartesianClos
     { isAdj := by
         haveI q : Exponentiable (e.inverse.obj X) := inferInstance
         have : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X)) := q.isAdj
-        have : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
-        apply NatIso.ofComponents _ _
-        · intro Y
-          apply asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫ _
-          apply prod.mapIso (Iso.refl _) (e.unitIso.app Y).symm
-        · intro Y Z g
-          dsimp
-          simp [prodComparison, prod.comp_lift, ← e.inverse.map_comp, ← e.inverse.map_comp_assoc]
-          -- I wonder if it would be a good idea to make `map_comp` a simp lemma the other way round
+        have : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅
+            prod.functor.obj (e.inverse.obj X) := by
+          apply NatIso.ofComponents _ _
+          · intro Y
+            apply asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫ _
+            apply prod.mapIso (Iso.refl _) (e.unitIso.app Y).symm
+          · intro Y Z g
+            dsimp
+            simp [prodComparison, prod.comp_lift, ← e.inverse.map_comp, ← e.inverse.map_comp_assoc]
+            -- I wonder if it would be a good idea to
+            -- make `map_comp` a simp lemma the other way round
         · have : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse) :=
             Adjunction.leftAdjointOfNatIso this.symm
           have : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) :=

Mathlib/CategoryTheory/ConnectedComponents.lean

@@ -136,9 +136,9 @@ instance : Full (decomposedTo J)
   preimage := by
     rintro ⟨j', X, hX⟩ ⟨k', Y, hY⟩ f
     dsimp at f
-    have : j' = k'
-    rw [← hX, ← hY, Quotient.eq'']
-    exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)
+    have : j' = k' := by
+      rw [← hX, ← hY, Quotient.eq'']
+      exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)
     subst this
     exact Sigma.SigmaHom.mk f
   witness := by

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

@@ -320,9 +320,9 @@ instance colimitLimitToLimitColimit_isIso : IsIso (colimitLimitToLimitColimit F)
 instance colimitLimitToLimitColimitCone_iso (F : J ⥤ K ⥤ Type v) :
     IsIso (colimitLimitToLimitColimitCone F) := by
   have : IsIso (colimitLimitToLimitColimitCone F).Hom := by
-    suffices : IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
-      lim.map (whiskerRight (currying.unitIso.app F).inv colim))
-    apply IsIso.comp_isIso
+    suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
+        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
+      apply IsIso.comp_isIso
     infer_instance
   apply Cones.cone_iso_of_hom_iso
 #align category_theory.limits.colimit_limit_to_limit_colimit_cone_iso CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso

Mathlib/CategoryTheory/Limits/Final.lean

@@ -759,8 +759,7 @@ theorem final_comp [hF : Final F] [hG : Final G] : Final (F ⋙ G) := by
   infer_instance
 
 theorem initial_comp [Initial F] [Initial G] : Initial (F ⋙ G) := by
-  suffices : Final (F ⋙ G).op
-  · exact initial_of_final_op _
+  suffices Final (F ⋙ G).op from initial_of_final_op _
   exact final_comp F.op G.op
 
 theorem final_of_final_comp [hF : Final F] [hFG : Final (F ⋙ G)] : Final G := by
@@ -780,8 +779,7 @@ theorem final_of_final_comp [hF : Final F] [hFG : Final (F ⋙ G)] : Final G :=
   exact fun H => IsIso.of_isIso_comp_left (colimit.pre _ (s₁.inverse ⋙ F ⋙ s₂.functor)) _
 
 theorem initial_of_initial_comp [Initial F] [Initial (F ⋙ G)] : Initial G := by
-  suffices : Final G.op
-  · exact initial_of_final_op _
+  suffices Final G.op from initial_of_final_op _
   have : Final (F.op ⋙ G.op) := show Final (F ⋙ G).op from inferInstance
   exact final_of_final_comp F.op G.op
 

Mathlib/CategoryTheory/Limits/KanExtension.lean

@@ -184,11 +184,11 @@ set_option linter.uppercaseLean3 false in
 
 theorem reflective [Full ι] [Faithful ι] [∀ X, HasLimitsOfShape (StructuredArrow X ι) D] :
     IsIso (adjunction D ι).counit := by
-  suffices : ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).counit X)
-  · apply NatIso.isIso_of_isIso_app
+  suffices ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).counit X) by
+    apply NatIso.isIso_of_isIso_app
   intro F
-  suffices : ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).counit F) X)
-  · apply NatIso.isIso_of_isIso_app
+  suffices ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).counit F) X) by
+    apply NatIso.isIso_of_isIso_app
   intro X
   dsimp [adjunction, equiv]
   simp only [Category.id_comp]
@@ -349,11 +349,11 @@ set_option linter.uppercaseLean3 false in
 
 theorem coreflective [Full ι] [Faithful ι] [∀ X, HasColimitsOfShape (CostructuredArrow ι X) D] :
     IsIso (adjunction D ι).unit := by
-  suffices : ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).unit X)
-  · apply NatIso.isIso_of_isIso_app
+  suffices ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).unit X) by
+    apply NatIso.isIso_of_isIso_app
   intro F
-  suffices : ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).unit F) X)
-  · apply NatIso.isIso_of_isIso_app
+  suffices ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).unit F) X) by
+    apply NatIso.isIso_of_isIso_app
   intro X
   dsimp [adjunction, equiv]
   simp only [Category.comp_id]

Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

@@ -107,8 +107,8 @@ def regularOfIsPullbackSndOfRegular {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h
   isLimit := by
     apply Fork.IsLimit.mk' _ _
     intro s
-    have l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ hr.right
-    rw [Category.assoc, s.condition, Category.assoc]
+    have l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ hr.right := by
+      rw [Category.assoc, s.condition, Category.assoc]
     obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hr.isLimit _ l₁
     obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl
     refine' ⟨p, hp₂, _⟩
@@ -244,8 +244,8 @@ def regularOfIsPushoutSndOfRegular {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h
   isColimit := by
     apply Cofork.IsColimit.mk' _ _
     intro s
-    have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
-    rw [← Category.assoc, ← Category.assoc, s.condition]
+    have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π := by
+      rw [← Category.assoc, ← Category.assoc, s.condition]
     obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' gr.isColimit (f ≫ Cofork.π s) l₁
     obtain ⟨p, hp₁, _⟩ := PushoutCocone.IsColimit.desc' t _ _ hl.symm
     refine' ⟨p, hp₁, _⟩

Mathlib/CategoryTheory/Limits/Shapes/Types.lean

@@ -497,8 +497,8 @@ theorem unique_of_type_equalizer (t : IsLimit (Fork.ofι _ w)) (y : Y) (hy : g y
   have hy' : y' ≫ g = y' ≫ h := funext fun _ => hy
   refine' ⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_fun (Fork.IsLimit.lift' t y' _).2 ⟨⟩, _⟩
   intro x' hx'
-  suffices : (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1
-  rw [← this]
+  suffices (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1 by
+    rw [← this]
   apply Fork.IsLimit.hom_ext t
   funext ⟨⟩
   apply hx'.trans (congr_fun (Fork.IsLimit.lift' t _ hy').2 ⟨⟩).symm

Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

@@ -310,8 +310,7 @@ def tensorLeftHomEquiv (X Y Y' Z : C) [ExactPairing Y Y'] : (Y' ⊗ X ⟶ Z) ≃
     have c :
       (α_ Y' (Y ⊗ Y') X).hom ≫
           (𝟙 Y' ⊗ (α_ Y Y' X).hom) ≫ (α_ Y' Y (Y' ⊗ X)).inv ≫ (α_ (Y' ⊗ Y) Y' X).inv =
-        (α_ _ _ _).inv ⊗ 𝟙 _
-    pure_coherence
+        (α_ _ _ _).inv ⊗ 𝟙 _ := by pure_coherence
     slice_lhs 4 7 => rw [c]
     slice_lhs 3 5 => rw [← comp_tensor_id, ← comp_tensor_id, coevaluation_evaluation]
     simp only [leftUnitor_conjugation]
@@ -325,8 +324,7 @@ def tensorLeftHomEquiv (X Y Y' Z : C) [ExactPairing Y Y'] : (Y' ⊗ X ⟶ Z) ≃
     have c :
       (α_ (Y ⊗ Y') Y Z).hom ≫
           (α_ Y Y' (Y ⊗ Z)).hom ≫ (𝟙 Y ⊗ (α_ Y' Y Z).inv) ≫ (α_ Y (Y' ⊗ Y) Z).inv =
-        (α_ _ _ _).hom ⊗ 𝟙 Z
-    pure_coherence
+        (α_ _ _ _).hom ⊗ 𝟙 Z := by pure_coherence
     slice_lhs 5 8 => rw [c]
     slice_lhs 4 6 => rw [← comp_tensor_id, ← comp_tensor_id, evaluation_coevaluation]
     simp only [leftUnitor_conjugation]
@@ -349,8 +347,7 @@ def tensorRightHomEquiv (X Y Y' Z : C) [ExactPairing Y Y'] : (X ⊗ Y ⟶ Z) ≃
     have c :
       (α_ X (Y ⊗ Y') Y).inv ≫
           ((α_ X Y Y').inv ⊗ 𝟙 Y) ≫ (α_ (X ⊗ Y) Y' Y).hom ≫ (α_ X Y (Y' ⊗ Y)).hom =
-        𝟙 _ ⊗ (α_ _ _ _).hom
-    pure_coherence
+        𝟙 _ ⊗ (α_ _ _ _).hom := by pure_coherence
     slice_lhs 4 7 => rw [c]
     slice_lhs 3 5 => rw [← id_tensor_comp, ← id_tensor_comp, evaluation_coevaluation]
     simp only [rightUnitor_conjugation]
@@ -364,8 +361,7 @@ def tensorRightHomEquiv (X Y Y' Z : C) [ExactPairing Y Y'] : (X ⊗ Y ⟶ Z) ≃
     have c :
       (α_ Z Y' (Y ⊗ Y')).inv ≫
           (α_ (Z ⊗ Y') Y Y').inv ≫ ((α_ Z Y' Y).hom ⊗ 𝟙 Y') ≫ (α_ Z (Y' ⊗ Y) Y').hom =
-        𝟙 _ ⊗ (α_ _ _ _).inv
-    pure_coherence
+        𝟙 _ ⊗ (α_ _ _ _).inv := by pure_coherence
     slice_lhs 5 8 => rw [c]
     slice_lhs 4 6 => rw [← id_tensor_comp, ← id_tensor_comp, coevaluation_evaluation]
     simp only [rightUnitor_conjugation]

Mathlib/CategoryTheory/Subobject/MonoOver.lean

@@ -434,8 +434,8 @@ instance faithful_exists (f : X ⟶ Y) : Faithful («exists» f) where
 def existsIsoMap (f : X ⟶ Y) [Mono f] : «exists» f ≅ map f :=
   NatIso.ofComponents (by
     intro Z
-    suffices : (forget _).obj ((«exists» f).obj Z) ≅ (forget _).obj ((map f).obj Z)
-    apply (forget _).preimageIso this
+    suffices (forget _).obj ((«exists» f).obj Z) ≅ (forget _).obj ((map f).obj Z) by
+      apply (forget _).preimageIso this
     apply Over.isoMk _ _
     apply imageMonoIsoSource (Z.arrow ≫ f)
     apply imageMonoIsoSource_hom_self)

Mathlib/Combinatorics/HalesJewett.lean

@@ -254,10 +254,10 @@ private theorem exists_mono_in_high_dimension' :
       ∀ r : ℕ,
         ∃ (ι : Type) (_ : Fintype ι),
           ∀ C : (ι → Option α) → κ,
-            (∃ s : ColorFocused C, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
-    -- Given the key claim, we simply take `r = |κ| + 1`. We cannot have this many distinct colors
-    -- so we must be in the second case, where there is a monochromatic line.
-    · obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
+            (∃ s : ColorFocused C, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l by
+      -- Given the key claim, we simply take `r = |κ| + 1`. We cannot have this many distinct colors
+      -- so we must be in the second case, where there is a monochromatic line.
+      obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
       refine' ⟨ι, _inst, fun C => (hι C).resolve_left _⟩
       rintro ⟨s, sr⟩
       apply Nat.not_succ_le_self (Fintype.card κ)

Mathlib/Computability/Primrec.lean

@@ -902,8 +902,8 @@ private theorem list_foldl' {f : α → List β} {g : α → σ} {h : α → σ
     (fst.comp <|
       nat_iterate (encode_iff.2 hf) (pair hg hf) <|
       hG)
-  suffices : ∀ a n, F a n = (((f a).take n).foldl (fun s b => h a (s, b)) (g a), (f a).drop n)
-  · refine hF.of_eq fun a => ?_
+  suffices ∀ a n, F a n = (((f a).take n).foldl (fun s b => h a (s, b)) (g a), (f a).drop n) by
+    refine hF.of_eq fun a => ?_
     rw [this, List.take_all_of_le (length_le_encode _)]
   introv
   dsimp only

Mathlib/Computability/TuringMachine.lean

@@ -1696,8 +1696,7 @@ def trNormal : Stmt₁ → Stmt'₁
 
 theorem stepAux_move (d : Dir) (q : Stmt'₁) (v : σ) (T : Tape Bool) :
     stepAux (moveₙ d q) v T = stepAux q v ((Tape.move d)^[n] T) := by
-  suffices : ∀ i, stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
-  exact this n
+  suffices ∀ i, stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T) from this n
   intro i; induction' i with i IH generalizing T; · rfl
   rw [iterate_succ', iterate_succ]
   simp only [stepAux, Function.comp_apply]

Mathlib/Control/Fix.lean

@@ -81,9 +81,9 @@ protected theorem fix_def {x : α} (h' : ∃ i, (Fix.approx f i x).Dom) :
   revert hk
   dsimp [Part.fix]; rw [assert_pos h']; revert this
   generalize Upto.zero = z; intro _this hk
-  suffices : ∀ x',
+  suffices ∀ x',
     WellFounded.fix (Part.fix.proof_1 f x h') (fixAux f) z x' = Fix.approx f (succ k) x'
-  exact this _
+    from this _
   induction k generalizing z with
   | zero =>
     intro x'

Mathlib/Control/LawfulFix.lean

@@ -77,8 +77,8 @@ theorem mem_iff (a : α) (b : β a) : b ∈ Part.fix f a ↔ ∃ i, b ∈ approx
     rw [dom_iff_mem] at h₁
     cases' h₁ with y h₁
     replace h₁ := approx_mono' f _ _ h₁
-    suffices : y = b
-    · subst this
+    suffices y = b by
+      subst this
       exact h₁
     cases' hh with i hh
     revert h₁; generalize succ (Nat.find h₀) = j; intro h₁

Mathlib/Data/Bitvec/Lemmas.lean

@@ -88,7 +88,7 @@ theorem toNat_eq_foldr_reverse {n : ℕ} (v : Bitvec n) :
 #align bitvec.to_nat_eq_foldr_reverse Bitvec.toNat_eq_foldr_reverse
 
 theorem toNat_lt {n : ℕ} (v : Bitvec n) : v.toNat < 2 ^ n := by
-  suffices : v.toNat + 1 ≤ 2 ^ n; simpa
+  suffices v.toNat + 1 ≤ 2 ^ n by simpa
   rw [toNat_eq_foldr_reverse]
   cases' v with xs h
   dsimp [Bitvec.toNat, bitsToNat]

Mathlib/Data/Bool/Count.lean

@@ -25,7 +25,7 @@ theorem count_not_add_count (l : List Bool) (b : Bool) : count (!b) l + count b
   -- Porting note: Proof re-written
   -- Old proof: simp only [length_eq_countP_add_countP (Eq (!b)), Bool.not_not_eq, count]
   simp only [length_eq_countP_add_countP (· == !b), count, add_right_inj]
-  suffices : (fun x => x == b) = (fun a => decide ¬(a == !b) = true); rw [this]
+  suffices (fun x => x == b) = (fun a => decide ¬(a == !b) = true) by rw [this]
   ext x; cases x <;> cases b <;> rfl
 #align list.count_bnot_add_count List.count_not_add_count
 

Mathlib/Data/FinEnum.lean

@@ -155,8 +155,8 @@ theorem Finset.mem_enum [DecidableEq α] (s : Finset α) (xs : List α) :
       simp only [or_iff_not_imp_left] at h
       exists h
       by_cases h : xs_hd ∈ s
-      · have : {xs_hd} ⊆ s
-        simp only [HasSubset.Subset, *, forall_eq, mem_singleton]
+      · have : {xs_hd} ⊆ s := by
+          simp only [HasSubset.Subset, *, forall_eq, mem_singleton]
         simp only [union_sdiff_of_subset this, or_true_iff, Finset.union_sdiff_of_subset,
           eq_self_iff_true]
       · left