awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
⊢ 𝓝 a = pure a ↔ ¬IsSuccLimit a

Tactic:
SuccOrder.nhds_eq_pure

Premises used: SuccOrder.nhds_eq_pure
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
⊢ IsOpen s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
SuccOrder.isOpen_iff

Premises used: SuccOrder.isOpen_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ a ∈ closure s

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ a ∈ closure (s ∩ Iic a)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)

Tactic:
simpa only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter',
      SuccOrder.nhdsLE_eq_nhds] using id

Premises used: SuccOrder.nhdsLE_eq_nhds, id, mem_closure_iff_nhdsWithin_neBot, Set.inter_comm, nhdsWithin_inter'
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)

Tactic:
tfae_have 1 → 2 := by
    simpa only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter',
      SuccOrder.nhdsLE_eq_nhds] using id
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
⊢ a ∈ closure (s ∩ Iic a)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
⊢ ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
h_1 : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := h_1
inl : ∀ (he : s ∩ Iic a = ∅), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
inr : ∀ (hne : (s ∩ Iic a).Nonempty), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne

Premises used: Inter.inter, Set.eq_empty_or_nonempty, Set.Iic
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
h_1 : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := h_1
he : s ∩ Iic a = ∅
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
simp [he] at h
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
h_1 : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := h_1
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩

Premises used: IsLUB.csSup_eq, And.intro, isLUB_of_mem_closure
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
h_1 : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := h_1
hne : (s ∩ Iic a).Nonempty
inr : a ∈ upperBounds (s ∩ Iic a)
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
h_1 : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := h_1
hne : (s ∩ Iic a).Nonempty
⊢ a ∈ upperBounds (s ∩ Iic a)

Tactic:
fun x hx => hx.2

Premises used: Set.Mem, setOf, upperBounds, And.right, Set.Iic
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
h_1 : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := h_1
hne : (s ∩ Iic a).Nonempty
⊢ a ∈ upperBounds (s ∩ Iic a)

Tactic:
exact fun x hx => hx.2
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
⊢ ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
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
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
⊢ ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
⊢ ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
⊢ ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a

Tactic:
tfae_have 3 → 4
  | h => ⟨_, inter_subset_left, h.1, bddAbove_Iic.mono inter_subset_right, h.2⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
⊢ ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
⊢ ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
⊢ ∀ (a_1 : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a),
    ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : BddAbove t
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
⊢ Small.{u, u + 1} (↑t : Type (u + 1))

Tactic:
rw [bddAbove_iff_small] at ht₁

Premises used: Ordinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : BddAbove t
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
ht₂ : Small.{u, u + 1} (↑t : Type (u + 1))
⊢ ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))

Tactic:
rw [bddAbove_iff_small] at ht₁

Premises used: Ordinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : BddAbove t
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
ht₂ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2₁ : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
⊢ ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t

Tactic:
rw [bddAbove_iff_small] at ht₁

Premises used: Ordinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : BddAbove t
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
ht₂ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2₁ : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3₁ :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
⊢ ∀ (a : (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

Tactic:
rw [bddAbove_iff_small] at ht₁

Premises used: Ordinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
⊢ ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = sSup t

Tactic:
⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩

Premises used: Function.comp, Set.Elem, And.intro, Exists.intro, Shrink, Equiv.symm, equivShrink, Subtype.val, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
refine_1 : Nonempty.{u + 1} (Shrink.{u, u + 1} (↑t : Type (u + 1)))
refine_2 :
  ∀ (i : Shrink.{u, u + 1} (↑t : Type (u + 1))),
    Function.comp (β := { x : Ordinal.{u} // x ∈ t }) (Subtype.val (p := fun (x : Ordinal.{u}) ↦ x ∈ t))
        (⇑(Equiv.symm (equivShrink (↑t : Type (u + 1)))) :
          (a : Shrink.{u, u + 1} (↑t : Type (u + 1))) → (↑t : Type (u + 1)))
        i ∈
      s
refine_3 :
  ⨆ (i : Shrink.{u, u + 1} (↑t : Type (u + 1))),
      Function.comp (β := { x : Ordinal.{u} // x ∈ t }) (Subtype.val (p := fun (x : Ordinal.{u}) ↦ x ∈ t))
        (⇑(Equiv.symm (equivShrink (↑t : Type (u + 1)))) :
          (a : Shrink.{u, u + 1} (↑t : Type (u + 1))) → (↑t : Type (u + 1)))
        i =
    sSup t
⊢ ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = sSup t

Tactic:
refine ⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
⊢ Nonempty.{u + 2} (↑t : Type (u + 1))

Tactic:
have := ht₀.to_subtype
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
this : Nonempty.{u + 2} (↑t : Type (u + 1))
⊢ Nonempty.{u + 1} (Shrink.{u, u + 1} (↑t : Type (u + 1)))

Tactic:
(equivShrink _).symm.nonempty

Premises used: Equiv.nonempty, Equiv.symm, equivShrink
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
this : Nonempty.{u + 2} (↑t : Type (u + 1))
⊢ Nonempty.{u + 1} (Shrink.{u, u + 1} (↑t : Type (u + 1)))

Tactic:
exact (equivShrink _).symm.nonempty

Premises used: Equiv.nonempty, Equiv.symm, equivShrink
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
⊢ ∀ (i : Shrink.{u, u + 1} (↑t : Type (u + 1))),
    Function.comp (β := { x : Ordinal.{u} // x ∈ t }) (Subtype.val (p := fun (x : Ordinal.{u}) ↦ x ∈ t))
        (⇑(Equiv.symm (equivShrink (↑t : Type (u + 1)))) :
          (a : Shrink.{u, u + 1} (↑t : Type (u + 1))) → (↑t : Type (u + 1)))
        i ∈
      s

Tactic:
simpa [← (equivShrink t).forall_congr_left (p := (·.1 ∈ s))]

Premises used: Equiv.forall_congr_left, Set.Elem, equivShrink
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} (↑t : Type (u + 1))
tfae_1_to_2 : ∀ (a : sSup t ∈ closure s), sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 :
  ∀ (a : sSup t ∈ closure (s ∩ Iic (sSup t))), (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  ∀ (a : (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
⊢ ⨆ (i : Shrink.{u, u + 1} (↑t : Type (u + 1))),
      Function.comp (β := { x : Ordinal.{u} // x ∈ t }) (Subtype.val (p := fun (x : Ordinal.{u}) ↦ x ∈ t))
        (⇑(Equiv.symm (equivShrink (↑t : Type (u + 1)))) :
          (a : Shrink.{u, u + 1} (↑t : Type (u + 1))) → (↑t : Type (u + 1)))
        i =
    sSup t

Tactic:
simp [(equivShrink t).symm.iSup_comp, ← sSup_eq_iSup']

Premises used: Equiv.iSup_comp, Set.Elem, Equiv.symm, equivShrink, sSup_eq_iSup'
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
⊢ ∀ (a_1 : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a),
    ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a

Tactic:
tfae_have 4 → 5 := by
    rintro ⟨t, ht, ht₀, ht₁, rfl⟩
    rw [bddAbove_iff_small] at ht₁
    refine ⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩
    · have := ht₀.to_subtype
      exact (equivShrink _).symm.nonempty
    · simpa [← (equivShrink t).forall_congr_left (p := (·.1 ∈ s))]
    · simp [(equivShrink t).symm.iSup_comp, ← sSup_eq_iSup']
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  ∀ (a_1 : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a),
    ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
⊢ ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  ∀ (a_1 : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a),
    ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
⊢ a ∈ closure s

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  ∀ (a_1 : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a),
    ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
⊢ ∀ (a_1 : ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a),
    a ∈ closure s

Tactic:
5 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
ι : Type u
hne : Nonempty ι
f : ι → Ordinal.{u}
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : ∀ (a : ⨆ (i : ι), f i ∈ closure s), ⨆ (i : ι), f i ∈ closure (s ∩ Iic (⨆ (i : ι), f i))
tfae_2_to_3 :
  ∀ (a : ⨆ (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 :
  ∀ (a : (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 :
  ∀ (a : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ (i : ι), f i),
    ∃ (ι_1 : Type u),
      Nonempty ι_1 ∧
        ∃ (f_1 : ι_1 → Ordinal.{u}),
          (∀ (i : ι_1), f_1 i ∈ s) ∧ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : ι_1), f_1 i) (⨆ (i : ι), f i)
⊢ ⨆ (i : ι), f i ∈ closure s

Tactic:
closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f)
      bddAbove_of_small

Premises used: Iff.mpr, closure_mono, Ordinal.bddAbove_of_small, Set.range_nonempty, csSup_mem_closure, Set.range_subset_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
ι : Type u
hne : Nonempty ι
f : ι → Ordinal.{u}
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : ∀ (a : ⨆ (i : ι), f i ∈ closure s), ⨆ (i : ι), f i ∈ closure (s ∩ Iic (⨆ (i : ι), f i))
tfae_2_to_3 :
  ∀ (a : ⨆ (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 :
  ∀ (a : (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 :
  ∀ (a : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ (i : ι), f i),
    ∃ (ι_1 : Type u),
      Nonempty ι_1 ∧
        ∃ (f_1 : ι_1 → Ordinal.{u}),
          (∀ (i : ι_1), f_1 i ∈ s) ∧ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : ι_1), 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_of_small

Premises used: Iff.mpr, closure_mono, Ordinal.bddAbove_of_small, Set.range_nonempty, csSup_mem_closure, Set.range_subset_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : ∀ (a_1 : a ∈ closure s), a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : ∀ (a_1 : a ∈ closure (s ∩ Iic a)), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : ∀ (a_1 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a), ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  ∀ (a_1 : ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a),
    ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
⊢ ∀ (a_1 : ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a),
    a ∈ closure s

Tactic:
tfae_have 5 → 1 := by
    rintro ⟨ι, hne, f, hfs, rfl⟩
    exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f)
      bddAbove_of_small