chore: stop using 'old-style' tfae_have syntax (#11000)

Banishes "Mathlib `have`" style syntax for `tfae_have` (but does not officially deprecate it). Since we now have the chance to supply a term after `tfae_have ... :=`, we remove one-line `exact`s where possible, and convert `intro`s and some `rintros` into match alternatives. Most single-line `fun`s are preserved.



Co-authored-by: Yury G. Kudryashov <[email protected]>

Mathlib/Algebra/Exact.lean

@@ -323,19 +323,17 @@ theorem Exact.split_tfae' (h : Function.Exact f g) :
       Function.Surjective g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
       ∃ e : N ≃ₗ[R] M × P, f = e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ e] := by
   tfae_have 1 → 3
-  · rintro ⟨hf, l, hl⟩
-    exact ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩
+  | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩
   tfae_have 2 → 3
-  · rintro ⟨hg, l, hl⟩
-    exact ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩
+  | ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩
   tfae_have 3 → 1
-  · rintro ⟨e, e₁, e₂⟩
+  | ⟨e, e₁, e₂⟩ => by
     have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
-    refine ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
+    exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
   tfae_have 3 → 2
-  · rintro ⟨e, e₁, e₂⟩
+  | ⟨e, e₁, e₂⟩ => by
     have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
-    refine ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
+    exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
   tfae_finish
 
 /-- Equivalent characterizations of split exact sequences. Also known as the **Splitting lemma**. -/
@@ -347,10 +345,10 @@ theorem Exact.split_tfae
       ∃ l, g ∘ₗ l = LinearMap.id,
       ∃ l, l ∘ₗ f = LinearMap.id,
       ∃ e : N ≃ₗ[R] M × P, f = e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ e] := by
-  tfae_have 1 ↔ 3
-  · simpa using (h.splitSurjectiveEquiv hf).nonempty_congr
-  tfae_have 2 ↔ 3
-  · simpa using (h.splitInjectiveEquiv hg).nonempty_congr
+  tfae_have 1 ↔ 3 := by
+    simpa using (h.splitSurjectiveEquiv hf).nonempty_congr
+  tfae_have 2 ↔ 3 := by
+    simpa using (h.splitInjectiveEquiv hg).nonempty_congr
   tfae_finish
 
 end split

Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean

@@ -116,7 +116,7 @@ lemma preservesFiniteLimits_tfae : List.TFAE
       Nonempty <| PreservesFiniteLimits F
     ] := by
   tfae_have 1 → 2
-  · rintro hF S ⟨hS, hf⟩
+  | hF, S, ⟨hS, hf⟩ => by
     have := preservesMonomorphisms_of_preserves_shortExact_left F hF
     refine ⟨?_, inferInstance⟩
     let T := ShortComplex.mk S.f (Abelian.coimage.π S.g) (Abelian.comp_coimage_π_eq_zero S.zero)
@@ -129,7 +129,7 @@ lemma preservesFiniteLimits_tfae : List.TFAE
     exact (exact_iff_of_epi_of_isIso_of_mono φ).1 (hF T ⟨(S.exact_iff_exact_coimage_π).1 hS⟩).1
 
   tfae_have 2 → 3
-  · intro hF X Y f
+  | hF, X, Y, f => by
     refine ⟨preservesLimitOfPreservesLimitCone (kernelIsKernel f) ?_⟩
     apply (KernelFork.isLimitMapConeEquiv _ F).2
     let S := ShortComplex.mk _ _ (kernel.condition f)
@@ -138,13 +138,13 @@ lemma preservesFiniteLimits_tfae : List.TFAE
     exact hS.1.fIsKernel
 
   tfae_have 3 → 4
-  · intro hF
+  | hF => by
     have := fun X Y (f : X ⟶ Y) ↦ (hF f).some
     exact ⟨preservesFiniteLimitsOfPreservesKernels F⟩
 
   tfae_have 4 → 1
-  · rintro ⟨_⟩ S hS
-    exact (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel F⟩
+  | ⟨_⟩, S, hS =>
+    (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel F⟩
 
   tfae_finish
 
@@ -175,7 +175,7 @@ lemma preservesFiniteColimits_tfae : List.TFAE
       Nonempty <| PreservesFiniteColimits F
     ] := by
   tfae_have 1 → 2
-  · rintro hF S ⟨hS, hf⟩
+  | hF, S, ⟨hS, hf⟩ => by
     have := preservesEpimorphisms_of_preserves_shortExact_right F hF
     refine ⟨?_, inferInstance⟩
     let T := ShortComplex.mk (Abelian.image.ι S.f) S.g (Abelian.image_ι_comp_eq_zero S.zero)
@@ -188,7 +188,7 @@ lemma preservesFiniteColimits_tfae : List.TFAE
     exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1
 
   tfae_have 2 → 3
-  · intro hF X Y f
+  | hF, X, Y, f => by
     refine ⟨preservesColimitOfPreservesColimitCocone (cokernelIsCokernel f) ?_⟩
     apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2
     let S := ShortComplex.mk _ _ (cokernel.condition f)
@@ -197,14 +197,13 @@ lemma preservesFiniteColimits_tfae : List.TFAE
     exact hS.1.gIsCokernel
 
   tfae_have 3 → 4
-  · intro hF
+  | hF => by
     have := fun X Y (f : X ⟶ Y) ↦ (hF f).some
     exact ⟨preservesFiniteColimitsOfPreservesCokernels F⟩
 
   tfae_have 4 → 1
-  · rintro ⟨_⟩ S hS
-    exact (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2
-      ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel F⟩
+  | ⟨_⟩, S, hS => (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2
+    ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel F⟩
 
   tfae_finish
 
@@ -224,7 +223,7 @@ lemma exact_tfae : List.TFAE
       Nonempty (PreservesFiniteLimits F) ∧ Nonempty (PreservesFiniteColimits F)
     ] := by
   tfae_have 1 → 3
-  · intro hF
+  | hF => by
     refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩
     · have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
         And.intro (hF S hS).exact (hF S hS).mono_f)
@@ -234,21 +233,19 @@ lemma exact_tfae : List.TFAE
       exact h f |>.some
 
   tfae_have 2 → 1
-  · intro hF S hS
+  | hF, S, hS => by
     have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
       hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
     have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
       hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
     exact ⟨hF S hS.exact⟩
 
   tfae_have 3 → 4
-  · rintro ⟨h⟩
-    exact ⟨⟨preservesFiniteLimitsOfPreservesHomology F⟩,
-      ⟨preservesFiniteColimitsOfPreservesHomology F⟩⟩
+  | ⟨h⟩ => ⟨⟨preservesFiniteLimitsOfPreservesHomology F⟩,
+    ⟨preservesFiniteColimitsOfPreservesHomology F⟩⟩
 
   tfae_have 4 → 2
-  · rintro ⟨⟨h1⟩, ⟨h2⟩⟩
-    exact fun _ h ↦ h.map F
+  | ⟨⟨h1⟩, ⟨h2⟩⟩, _, h => h.map F
 
   tfae_finish
 

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -517,23 +517,23 @@ theorem tfae_modEq :
       [a ≡ b [PMOD p], ∀ z : ℤ, b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
         toIcoMod hp a b + p = toIocMod hp a b] := by
   rw [modEq_iff_toIcoMod_eq_left hp]
-  tfae_have 3 → 2
-  · rw [← not_exists, not_imp_not]
+  tfae_have 3 → 2 := by
+    rw [← not_exists, not_imp_not]
     exact fun ⟨i, hi⟩ =>
       ((toIcoMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ico_self hi, i, (sub_add_cancel b _).symm⟩).trans
         ((toIocMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ioc_self hi, i, (sub_add_cancel b _).symm⟩).symm
   tfae_have 4 → 3
-  · intro h
+  | h => by
     rw [← h, Ne, eq_comm, add_right_eq_self]
     exact hp.ne'
   tfae_have 1 → 4
-  · intro h
+  | h => by
     rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]
     refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
     rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]
     conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
-  tfae_have 2 → 1
-  · rw [← not_exists, not_imp_comm]
+  tfae_have 2 → 1 := by
+    rw [← not_exists, not_imp_comm]
     have h' := toIcoMod_mem_Ico hp a b
     exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩
   tfae_finish

Mathlib/Analysis/BoxIntegral/Box/Basic.lean

@@ -140,15 +140,12 @@ theorem le_def : I ≤ J ↔ ∀ x ∈ I, x ∈ J := Iff.rfl
 
 theorem le_TFAE : List.TFAE [I ≤ J, (I : Set (ι → ℝ)) ⊆ J,
     Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper] := by
-  tfae_have 1 ↔ 2
-  · exact Iff.rfl
+  tfae_have 1 ↔ 2 := Iff.rfl
   tfae_have 2 → 3
-  · intro h
-    simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h
-  tfae_have 3 ↔ 4
-  · exact Icc_subset_Icc_iff I.lower_le_upper
+  | h => by simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h
+  tfae_have 3 ↔ 4 := Icc_subset_Icc_iff I.lower_le_upper
   tfae_have 4 → 2
-  · exact fun h x hx i ↦ Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)
+  | h, x, hx, i => Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)
   tfae_finish
 
 variable {I J}

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -1671,8 +1671,8 @@ theorem norm_inner_eq_norm_tfae (x y : E) :
       x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x,
       x = 0 ∨ ∃ r : 𝕜, y = r • x,
       x = 0 ∨ y ∈ 𝕜 ∙ x] := by
-  tfae_have 1 → 2
-  · refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_
+  tfae_have 1 → 2 := by
+    refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_
     have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀)
     rw [← sq_eq_sq, mul_pow, ← mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h <;>
       try positivity
@@ -1682,13 +1682,12 @@ theorem norm_inner_eq_norm_tfae (x y : E) :
       sub_eq_zero] at h
     rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]
     rwa [inner_self_ne_zero]
-  tfae_have 2 → 3
-  · exact fun h => h.imp_right fun h' => ⟨_, h'⟩
-  tfae_have 3 → 1
-  · rintro (rfl | ⟨r, rfl⟩) <;>
+  tfae_have 2 → 3 := fun h => h.imp_right fun h' => ⟨_, h'⟩
+  tfae_have 3 → 1 := by
+    rintro (rfl | ⟨r, rfl⟩) <;>
     simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K, inner_self_eq_norm_mul_norm,
       sq, mul_left_comm]
-  tfae_have 3 ↔ 4; · simp only [Submodule.mem_span_singleton, eq_comm]
+  tfae_have 3 ↔ 4 := by simp only [Submodule.mem_span_singleton, eq_comm]
   tfae_finish
 
 /-- If the inner product of two vectors is equal to the product of their norms, then the two vectors

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -623,14 +623,11 @@ protected theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*}
   clear u hu hq
   -- Now we can prove the equivalence in this setting
   simp only [List.map]
-  tfae_have 1 → 3
-  · exact uniformEquicontinuous_of_equicontinuousAt_zero f
-  tfae_have 3 → 2
-  · exact UniformEquicontinuous.equicontinuous
-  tfae_have 2 → 1
-  · exact fun H ↦ H 0
+  tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
+  tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
+  tfae_have 2 → 1 := fun H ↦ H 0
   tfae_have 3 → 5
-  · intro H
+  | H => by
     have : ∀ᶠ x in 𝓝 0, ∀ k, q i (f k x) ≤ 1 := by
       filter_upwards [Metric.equicontinuousAt_iff_right.mp (H.equicontinuous 0) 1 one_pos]
         with x hx k
@@ -642,11 +639,10 @@ protected theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*}
     refine ⟨bdd, Seminorm.continuous' (r := 1) ?_⟩
     filter_upwards [this] with x hx
     simpa only [closedBall_iSup bdd _ one_pos, mem_iInter, mem_closedBall_zero] using hx
-  tfae_have 5 → 4
-  · exact fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩
+  tfae_have 5 → 4 := fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩
   tfae_have 4 → 1 -- This would work over any `NormedField`
-  · intro ⟨p, hp, hfp⟩
-    exact Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <|
+  | ⟨p, hp, hfp⟩ =>
+    Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <|
       Eventually.of_forall fun x k ↦ by simpa using hfp k x
   tfae_finish
 

Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

@@ -313,33 +313,30 @@ protected theorem NormedSpace.equicontinuous_TFAE : List.TFAE
       BddAbove (Set.range (‖f ·‖)),
       (⨆ i, (‖f i‖₊ : ENNReal)) < ⊤ ] := by
   -- `1 ↔ 2 ↔ 3` follows from `uniformEquicontinuous_of_equicontinuousAt_zero`
-  tfae_have 1 → 3
-  · exact uniformEquicontinuous_of_equicontinuousAt_zero f
-  tfae_have 3 → 2
-  · exact UniformEquicontinuous.equicontinuous
-  tfae_have 2 → 1
-  · exact fun H ↦ H 0
+  tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
+  tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
+  tfae_have 2 → 1 := fun H ↦ H 0
   -- `4 ↔ 5 ↔ 6 ↔ 7 ↔ 8 ↔ 9` is morally trivial, we just have to use a lot of rewriting
   -- and `congr` lemmas
-  tfae_have 4 ↔ 5
-  · rw [exists_ge_and_iff_exists]
+  tfae_have 4 ↔ 5 := by
+    rw [exists_ge_and_iff_exists]
     exact fun C₁ C₂ hC ↦ forall₂_imp fun i x ↦ le_trans' <| by gcongr
-  tfae_have 5 ↔ 7
-  · refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_)
+  tfae_have 5 ↔ 7 := by
+    refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_)
     rw [ContinuousLinearMap.opNorm_le_iff hC]
-  tfae_have 7 ↔ 8
-  · simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range]
-  tfae_have 6 ↔ 8
-  · simp_rw [bddAbove_def, Set.forall_mem_range]
-  tfae_have 8 ↔ 9
-  · rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp]
+  tfae_have 7 ↔ 8 := by
+    simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range]
+  tfae_have 6 ↔ 8 := by
+    simp_rw [bddAbove_def, Set.forall_mem_range]
+  tfae_have 8 ↔ 9 := by
+    rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp]
     rfl
   -- `3 ↔ 4` is the interesting part of the result. It is essentially a combination of
   -- `WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm` which turns
   -- equicontinuity into existence of some continuous seminorm and
   -- `Seminorm.bound_of_continuous_normedSpace` which characterize such seminorms.
-  tfae_have 3 ↔ 4
-  · refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
+  tfae_have 3 ↔ 4 := by
+    refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
       ?_
     rw [forall_const]
     constructor

Mathlib/Analysis/RCLike/Basic.lean

@@ -317,16 +317,14 @@ open List in
 /-- There are several equivalent ways to say that a number `z` is in fact a real number. -/
 theorem is_real_TFAE (z : K) : TFAE [conj z = z, ∃ r : ℝ, (r : K) = z, ↑(re z) = z, im z = 0] := by
   tfae_have 1 → 4
-  · intro h
+  | h => by
     rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
       ofReal_zero]
   tfae_have 4 → 3
-  · intro h
+  | h => by
     conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
-  tfae_have 3 → 2
-  · exact fun h => ⟨_, h⟩
-  tfae_have 2 → 1
-  · exact fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
+  tfae_have 3 → 2 := fun h => ⟨_, h⟩
+  tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
   tfae_finish
 
 theorem conj_eq_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -130,29 +130,24 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
     fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩
   have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A
   -- First we prove that 1-4 are equivalent using 2 → 3 → 4, 1 → 3, and 2 → 1
-  tfae_have 1 → 3
-  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
-  tfae_have 2 → 1
-  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
+  tfae_have 1 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
+  tfae_have 2 → 1 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
   tfae_have 3 → 2
-  · rintro ⟨a, ha, H⟩
+  | ⟨a, ha, H⟩ => by
     rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩
     exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
       H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩
-  tfae_have 2 → 4
-  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
-  tfae_have 4 → 3
-  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
+  tfae_have 2 → 4 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
+  tfae_have 4 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
   -- Add 5 and 6 using 4 → 6 → 5 → 3
   tfae_have 4 → 6
-  · rintro ⟨a, ha, H⟩
+  | ⟨a, ha, H⟩ => by
     rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩
     refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩
     simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')
-  tfae_have 6 → 5
-  · exact fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩
+  tfae_have 6 → 5 := fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩
   tfae_have 5 → 3
-  · rintro ⟨a, ha, C, h₀, H⟩
+  | ⟨a, ha, C, h₀, H⟩ => by
     rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
     · obtain rfl : f = 0 := by
         ext n
@@ -163,19 +158,15 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
       isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩
   -- Add 7 and 8 using 2 → 8 → 7 → 3
   tfae_have 2 → 8
-  · rintro ⟨a, ha, H⟩
+  | ⟨a, ha, H⟩ => by
     refine ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩
     rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn
-  tfae_have 8 → 7
-  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩
+  tfae_have 8 → 7 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩
   tfae_have 7 → 3
-  · rintro ⟨a, ha, H⟩
+  | ⟨a, ha, H⟩ => by
     have : 0 ≤ a := nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)
     refine ⟨a, A ⟨this, ha⟩, IsBigO.of_bound 1 ?_⟩
     simpa only [Real.norm_eq_abs, one_mul, abs_pow, abs_of_nonneg this]
-  -- Porting note: used to work without explicitly having 6 → 7
-  tfae_have 6 → 7
-  · exact fun h ↦ tfae_8_to_7 <| tfae_2_to_8 <| tfae_3_to_2 <| tfae_5_to_3 <| tfae_6_to_5 h
   tfae_finish
 
 /-- For any natural `k` and a real `r > 1` we have `n ^ k = o(r ^ n)` as `n → ∞`. -/