-- 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
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) → a ∈ closure s

Tactic:
rintro ⟨ι, hne, f, hfs, rfl⟩

Result:
case intro.intro.intro.intro
s : Set Ordinal.{u}
ι : Type u
hne : Nonempty ι
f : ι → Ordinal.{u}
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : ⨆ i, f i ∈ closure s → ⨆ i, f i ∈ closure (s ∩ Iic (⨆ i, f i))
tfae_2_to_3 :
  ⨆ i, f i ∈ closure (s ∩ Iic (⨆ i, f i)) → (s ∩ Iic (⨆ i, f i)).Nonempty ∧ sSup (s ∩ Iic (⨆ i, f i)) = ⨆ i, f i
tfae_3_to_4 :
  (s ∩ Iic (⨆ i, f i)).Nonempty ∧ sSup (s ∩ Iic (⨆ i, f i)) = ⨆ i, f i →
    ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ i, f i
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ i, f i) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ o.bsup f_1 = ⨆ i, f i
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ o.bsup f_1 = ⨆ i, f i) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ ⨆ i, f_1 i = ⨆ i, f i
⊢ ⨆ i, f i ∈ closure s

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
⊢ (∃ 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

Tactic:
rintro ⟨o, h₀, f, hfs, rfl⟩

Result:
case intro.intro.intro.intro
s : Set Ordinal.{u}
o : Ordinal.{u}
h₀ : o ≠ 0
f : (x : Ordinal.{u}) → x < o → Ordinal.{u}
hfs : ∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s
tfae_1_to_2 : o.bsup f ∈ closure s → o.bsup f ∈ closure (s ∩ Iic (o.bsup f))
tfae_2_to_3 :
  o.bsup f ∈ closure (s ∩ Iic (o.bsup f)) → (s ∩ Iic (o.bsup f)).Nonempty ∧ sSup (s ∩ Iic (o.bsup f)) = o.bsup f
tfae_3_to_4 :
  (s ∩ Iic (o.bsup f)).Nonempty ∧ sSup (s ∩ Iic (o.bsup f)) = o.bsup f →
    ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = o.bsup f
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = o.bsup f) →
    ∃ o_1, o_1 ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o_1), f_1 x hx ∈ s) ∧ o_1.bsup f_1 = o.bsup f
⊢ ∃ ι, Nonempty ι ∧ ∃ f_1, (∀ (i : ι), f_1 i ∈ s) ∧ ⨆ i, f_1 i = o.bsup f

Proof state:
case intro.intro.intro.intro.refine_1
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}
x✝ : x < succ (sSup t)
⊢ (fun x x_1 => if x ∈ t then x else y) x x✝ ∈ s

Tactic:
simp only

Result:
case intro.intro.intro.intro.refine_1
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}
x✝ : x < succ (sSup t)
⊢ (if x ∈ t then x else y) ∈ s

Proof state:
case intro.intro.intro.intro
s : Set Ordinal.{u}
o : Ordinal.{u}
h₀ : o ≠ 0
f : (x : Ordinal.{u}) → x < o → Ordinal.{u}
hfs : ∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s
tfae_1_to_2 : o.bsup f ∈ closure s → o.bsup f ∈ closure (s ∩ Iic (o.bsup f))
tfae_2_to_3 :
  o.bsup f ∈ closure (s ∩ Iic (o.bsup f)) → (s ∩ Iic (o.bsup f)).Nonempty ∧ sSup (s ∩ Iic (o.bsup f)) = o.bsup f
tfae_3_to_4 :
  (s ∩ Iic (o.bsup f)).Nonempty ∧ sSup (s ∩ Iic (o.bsup f)) = o.bsup f →
    ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = o.bsup f
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = o.bsup f) →
    ∃ o_1, o_1 ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o_1), f_1 x hx ∈ s) ∧ o_1.bsup f_1 = o.bsup f
⊢ ∃ ι, Nonempty ι ∧ ∃ f_1, (∀ (i : ι), f_1 i ∈ s) ∧ ⨆ i, f_1 i = o.bsup f

Tactic:
exact ⟨_, toType_nonempty_iff_ne_zero.2 h₀, familyOfBFamily o f, fun _ => hfs _ _, rfl⟩

Result:
no goals

Proof state:
a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ [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 1 → 2 := by
  simpa only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter',
    SuccOrder.nhdsLE_eq_nhds] using id

Result:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic 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 intro.intro.intro.intro
s : Set Ordinal.{u}
ι : Type u
hne : Nonempty ι
f : ι → Ordinal.{u}
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : ⨆ i, f i ∈ closure s → ⨆ i, f i ∈ closure (s ∩ Iic (⨆ i, f i))
tfae_2_to_3 :
  ⨆ i, f i ∈ closure (s ∩ Iic (⨆ i, f i)) → (s ∩ Iic (⨆ i, f i)).Nonempty ∧ sSup (s ∩ Iic (⨆ i, f i)) = ⨆ i, f i
tfae_3_to_4 :
  (s ∩ Iic (⨆ i, f i)).Nonempty ∧ sSup (s ∩ Iic (⨆ i, f i)) = ⨆ i, f i →
    ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ i, f i
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ i, f i) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ o.bsup f_1 = ⨆ i, f i
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ o.bsup f_1 = ⨆ i, f i) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ ⨆ i, f_1 i = ⨆ i, f i
⊢ ⨆ i, f i ∈ closure s

Tactic:
exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f)
  (bddAbove_range.{u, u} f)

Result:
no goals