-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) :
    TFAE [a ∈ closure s,
      a ∈ closure (s ∩ Iic a),
      (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ t.Nonempty ∧ BddAbove t ∧ sSup t = a,
      ∃ (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) ∧ ⨆ i, f i = a]

Proof state:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
tfae_6_to_1 : (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) → a ∈ closure s
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2.refine_2
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : t.Nonempty
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal.{u}
hyt : y ∈ t
x : Ordinal.{u}
hx : x ∈ t
⊢ x ≤ (succ (sSup t)).bsup fun x x_1 => if x ∈ t then x else y

Tactic:
refine (if_pos hx).symm.trans_le (le_bsup _ _ <| (hlub.1 hx).trans_lt (lt_succ _))

Result:
no goals

Proof state:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE

Tactic:
tfae_have 5 → 6 := by
  rintro ⟨o, h₀, f, hfs, rfl⟩
  exact ⟨_, toType_nonempty_iff_ne_zero.2 h₀, familyOfBFamily o f, fun _ => hfs _ _, rfl⟩

Result:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE

Proof state:
case inl
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
he : s ∩ Iic a = ∅
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
simp [he] at h

Result:
no goals