diff --git a/Mathlib/Order/CompactlyGenerated.lean b/Mathlib/Order/CompactlyGenerated.lean
index 192843338a8bb..c064a6f4813eb 100644
--- a/Mathlib/Order/CompactlyGenerated.lean
+++ b/Mathlib/Order/CompactlyGenerated.lean
@@ -16,7 +16,7 @@ import Mathlib.Order.Zorn
 import Mathlib.Data.Finset.Order
 import Mathlib.Data.Set.Intervals.OrderIso
 import Mathlib.Data.Finite.Set
-import Mathlib.Data.List.TFAE
+import Mathlib.Tactic.TFAE
 
 /-!
 # Compactness properties for complete lattices
@@ -286,23 +286,15 @@ open List in
 theorem wellFounded_characterisations : List.TFAE
     [WellFounded (( · > · ) : α → α → Prop),
       IsSupFiniteCompact α, IsSupClosedCompact α, ∀ k : α, IsCompactElement k] := by
-  have h12 := WellFounded.isSupFiniteCompact α
-  have h23 := IsSupFiniteCompact.isSupClosedCompact α
-  have h31 := IsSupClosedCompact.wellFounded α
-  have h24 := isSupFiniteCompact_iff_all_elements_compact α
-  apply_rules [tfae_of_cycle, Chain.cons, Chain.nil] <;> dsimp only [ilast']
-  · rw [← h24]; exact h12 ∘ h31
-  · rw [← h24]; exact h31 ∘ h23
-  -- Porting note: proof using `tfae`
-  -- tfae_have 1 → 2
-  -- · exact WellFounded.isSupFiniteCompact α
-  -- tfae_have 2 → 3
-  -- · exact IsSupFiniteCompact.isSupClosedCompact α
-  -- tfae_have 3 → 1
-  -- · exact IsSupClosedCompact.wellFounded α
-  -- tfae_have 2 ↔ 4
-  -- · exact isSupFiniteCompact_iff_all_elements_compact α
-  -- tfae_finish
+  tfae_have 1 → 2
+  · exact WellFounded.isSupFiniteCompact α
+  tfae_have 2 → 3
+  · exact IsSupFiniteCompact.isSupClosedCompact α
+  tfae_have 3 → 1
+  · exact IsSupClosedCompact.wellFounded α
+  tfae_have 2 ↔ 4
+  · exact isSupFiniteCompact_iff_all_elements_compact α
+  tfae_finish
 #align complete_lattice.well_founded_characterisations CompleteLattice.wellFounded_characterisations
 
 theorem wellFounded_iff_isSupFiniteCompact :
diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean
index ba00e1fcf21f1..cac7fdf6a1940 100644
--- a/Mathlib/Order/WellFoundedSet.lean
+++ b/Mathlib/Order/WellFoundedSet.lean
@@ -11,7 +11,7 @@ Authors: Aaron Anderson
 import Mathlib.Order.Antichain
 import Mathlib.Order.OrderIsoNat
 import Mathlib.Order.WellFounded
-import Mathlib.Data.List.TFAE
+import Mathlib.Tactic.TFAE
 
 /-!
 # Well-founded sets
@@ -117,15 +117,18 @@ theorem acc_iff_wellFoundedOn {α} {r : α → α → Prop} {a : α} :
     TFAE [Acc r a,
       WellFoundedOn { b | ReflTransGen r b a } r,
       WellFoundedOn { b | TransGen r b a } r] := by
-  apply_rules [tfae_of_cycle, Chain.cons, Chain.nil] <;> dsimp only [ilast']
+  tfae_have 1 → 2
   · refine fun h => ⟨fun b => InvImage.accessible _ ?_⟩
     rw [← acc_transGen_iff] at h ⊢
     obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2
     · rwa [h'] at h
     · exact h.inv h'
+  tfae_have 2 → 3
   · exact fun h => h.subset fun _ => TransGen.to_reflTransGen
+  tfae_have 3 → 1
   · refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
     exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩
+  tfae_finish
 #align set.well_founded_on.acc_iff_well_founded_on Set.WellFoundedOn.acc_iff_wellFoundedOn
 
 end WellFoundedOn
@@ -808,4 +811,3 @@ theorem Pi.isPwo {α : ι → Type _} [∀ i, LinearOrder (α i)] [∀ i, IsWell
     refine' ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 _⟩
     exact ⟨hg (OrderHomClass.mono g' hab), hg' hab⟩
 #align pi.is_pwo Pi.isPwo
-
diff --git a/Mathlib/SetTheory/Ordinal/Topology.lean b/Mathlib/SetTheory/Ordinal/Topology.lean
index 1fd763005713f..0a866facf2213 100644
--- a/Mathlib/SetTheory/Ordinal/Topology.lean
+++ b/Mathlib/SetTheory/Ordinal/Topology.lean
@@ -9,6 +9,7 @@ Authors: Violeta Hernández Palacios
 ! if you have ported upstream changes.
 -/
 import Mathlib.SetTheory.Ordinal.Arithmetic
+import Mathlib.Tactic.TFAE
 import Mathlib.Topology.Order.Basic
 
 /-!
@@ -93,15 +94,18 @@ theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) :
       ∃ (o : Ordinal.{u}), o ≠ 0 ∧ ∃ (f : ∀ x < o, Ordinal),
         (∀ x hx, f x hx ∈ s) ∧ bsup.{u, u} o f = a,
       ∃ (ι : Type u), Nonempty ι ∧ ∃ f : ι → Ordinal, (∀ i, f i ∈ s) ∧ sup.{u, u} f = a] := by
-  apply_rules [tfae_of_cycle, Chain.cons, Chain.nil]
+  tfae_have 1 → 2
   · simp only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter', nhds_left_eq_nhds]
     exact id
+  tfae_have 2 → 3
   · intro h
     cases' (s ∩ Iic a).eq_empty_or_nonempty with he hne
     · simp [he] at h
     · refine ⟨hne, (isLUB_of_mem_closure ?_ h).csupₛ_eq hne⟩
       exact fun x hx => hx.2
+  tfae_have 3 → 4
   · exact fun h => ⟨_, inter_subset_left _ _, h.1, bddAbove_Iic.mono (inter_subset_right _ _), h.2⟩
+  tfae_have 4 → 5
   · rintro ⟨t, hts, hne, hbdd, rfl⟩
     have hlub : IsLUB t (supₛ t) := isLUB_csupₛ hne hbdd
     let ⟨y, hyt⟩ := hne
@@ -112,12 +116,15 @@ theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) :
       · refine le_antisymm (bsup_le fun x _ => ?_) (csupₛ_le hne fun x hx => ?_)
         · split_ifs <;> exact hlub.1 ‹_›
         · refine (if_pos hx).symm.trans_le (le_bsup _ _ <| (hlub.1 hx).trans_lt (lt_succ _))
+  tfae_have 5 → 6
   · rintro ⟨o, h₀, f, hfs, rfl⟩
     exact ⟨_, out_nonempty_iff_ne_zero.2 h₀, familyOfBFamily o f, fun _ => hfs _ _, rfl⟩
+  tfae_have 6 → 1
   · rintro ⟨ι, hne, f, hfs, rfl⟩
     rw [sup, supᵢ]
     exact closure_mono (range_subset_iff.2 hfs) <| csupₛ_mem_closure (range_nonempty f)
       (bddAbove_range.{u, u} f)
+  tfae_finish
 
 theorem mem_closure_iff_sup :
     a ∈ closure s ↔
@@ -233,4 +240,3 @@ theorem enumOrd_isNormal_iff_isClosed (hs : s.Unbounded (· < ·)) :
 #align ordinal.enum_ord_is_normal_iff_is_closed Ordinal.enumOrd_isNormal_iff_isClosed
 
 end Ordinal
-
diff --git a/Mathlib/Topology/LocallyConstant/Basic.lean b/Mathlib/Topology/LocallyConstant/Basic.lean
index 13776e6be56f7..f46f3cdc309e9 100644
--- a/Mathlib/Topology/LocallyConstant/Basic.lean
+++ b/Mathlib/Topology/LocallyConstant/Basic.lean
@@ -13,6 +13,7 @@ import Mathlib.Topology.Connected
 import Mathlib.Topology.ContinuousFunction.Basic
 import Mathlib.Algebra.IndicatorFunction
 import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.TFAE
 
 /-!
 # Locally constant functions
@@ -50,33 +51,19 @@ protected theorem tfae (f : X → Y) :
       ∀ x, IsOpen { x' | f x' = f x },
       ∀ y, IsOpen (f ⁻¹' {y}),
       ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x] := by
-  apply_rules [tfae_of_cycle, Chain.cons, Chain.nil]
-  · exact fun h x => (h {f x}).mem_nhds rfl
-  · exact fun h x => isOpen_iff_mem_nhds.2 fun y (hy : f y = f x) => hy ▸ h _
-  · intro h y
-    rcases em (y ∈ range f) with (⟨x, rfl⟩ | hy)
-    · exact h x
-    · simp only [preimage_eq_empty (disjoint_singleton_left.2 hy), isOpen_empty]
+  tfae_have 1 → 4; exact fun h y => h {y}
+  tfae_have 4 → 3; exact fun h x => h (f x)
+  tfae_have 3 → 2; exact fun h x => IsOpen.mem_nhds (h x) rfl
+  tfae_have 2 → 5
   · intro h x
-    rcases mem_nhds_iff.1 ((h (f x)).mem_nhds rfl) with ⟨U, hUf, hU, hx⟩
-    exact ⟨U, hU, hx, hUf⟩
-  · refine fun h s => isOpen_iff_forall_mem_open.2 fun x hx => ?_
-    rcases h x with ⟨U, hUo, hxU, hUf⟩
-    exact ⟨U, fun z hz => mem_preimage.2 <| (hUf z hz).symm ▸ hx, hUo, hxU⟩
-  -- porting note: todo: use `tfae_have`/`tfae_finish`; auto translated code below
-  -- tfae_have 1 → 4; exact fun h y => h {y}
-  -- tfae_have 4 → 3; exact fun h x => h (f x)
-  -- tfae_have 3 → 2; exact fun h x => IsOpen.mem_nhds (h x) rfl
-  -- tfae_have 2 → 5
-  -- · intro h x
-  --   rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩
-  --   exact ⟨U, hU, hx, Eq⟩
-  -- tfae_have 5 → 1
-  -- · intro h s
-  --   refine' isOpen_iff_forall_mem_open.2 fun x hx => _
-  --   rcases h x with ⟨U, hU, hxU, eq⟩
-  --   exact ⟨U, fun x' hx' => mem_preimage.2 <| (Eq x' hx').symm ▸ hx, hU, hxU⟩
-  -- tfae_finish
+    rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩
+    exact ⟨U, hU, hx, eq⟩
+  tfae_have 5 → 1
+  · intro h s
+    refine' isOpen_iff_forall_mem_open.2 fun x hx => _
+    rcases h x with ⟨U, hU, hxU, eq⟩
+    exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩
+  tfae_finish
 #align is_locally_constant.tfae IsLocallyConstant.tfae
 
 @[nontriviality]
diff --git a/Mathlib/Topology/NoetherianSpace.lean b/Mathlib/Topology/NoetherianSpace.lean
index 0051ceeb1b5bd..9cd2ce12f3e2f 100644
--- a/Mathlib/Topology/NoetherianSpace.lean
+++ b/Mathlib/Topology/NoetherianSpace.lean
@@ -86,23 +86,22 @@ instance NoetherianSpace.set [NoetherianSpace α] (s : Set α) : NoetherianSpace
 
 variable (α)
 
-example (α : Type _) : Set α ≃o (Set α)ᵒᵈ := by refine' OrderIso.compl (Set α)
-
 open List in
 theorem noetherianSpace_TFAE :
     TFAE [NoetherianSpace α,
       WellFounded fun s t : Closeds α => s < t,
       ∀ s : Set α, IsCompact s,
       ∀ s : Opens α, IsCompact (s : Set α)] := by
-  have h12 : NoetherianSpace α ↔ WellFounded fun s t : Closeds α => s < t
+  tfae_have 1 ↔ 2
   · refine' (noetherianSpace_iff α).trans (Surjective.wellFounded_iff Opens.compl_bijective.2 _)
     exact (@OrderIso.compl (Set α)).lt_iff_lt.symm
-  rw [← h12]
-  apply_rules [tfae_of_cycle, Chain.cons, Chain.nil]
-  · exact id
+  tfae_have 1 ↔ 4
+  · exact noetherianSpace_iff_opens α
+  tfae_have 1 → 3
   · exact @NoetherianSpace.isCompact α _
+  tfae_have 3 → 4
   · exact fun h s => h s
-  · exact (noetherianSpace_iff_opens α).2
+  tfae_finish
 #align topological_space.noetherian_space_tfae TopologicalSpace.noetherianSpace_TFAE
 
 variable {α}