Lean4
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] :=
by
tfae_have 1 → 2 := by
simpa only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter', SuccOrder.nhdsLE_eq_nhds] using id
tfae_have 2 → 3
| h => by
rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne
· simp [he] at h
· refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
exact fun x hx => hx.2
tfae_have 3 → 4
| h => ⟨_, inter_subset_left, h.1, bddAbove_Iic.mono inter_subset_right, h.2⟩
tfae_have 4 → 5 := by
rintro ⟨t, hts, hne, hbdd, rfl⟩
have hlub : IsLUB t (sSup t) := isLUB_csSup hne hbdd
let ⟨y, hyt⟩ := hne
classical
refine ⟨succ (sSup t), succ_ne_zero _, fun x _ => if x ∈ t then x else y, fun x _ => ?_, ?_⟩
· simp only
split_ifs with h <;> exact hts ‹_›
· refine le_antisymm (bsup_le fun x _ => ?_) (csSup_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 := by
rintro ⟨o, h₀, f, hfs, rfl⟩
exact ⟨_, toType_nonempty_iff_ne_zero.2 h₀, familyOfBFamily o f, fun _ => hfs _ _, rfl⟩
tfae_have 6 → 1 := by
rintro ⟨ι, hne, f, hfs, rfl⟩
exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f) (bddAbove_range.{u, u} f)
tfae_finish
