awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
b : α
hb : r b a
ho : o ≤ rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have inr : ∀ (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry ≤ ha_1.rank (r := r))
  (IH :
    ∀ (y : α) (a_2 : r y a)
      (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry < sorry.rank (r := r)),
      ∃ (b_1 : α) (hb_1 : Acc r b_1),
        hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry)
  (ho :
    rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry ≤
      rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry),
  ∃ (b_1 : α) (hb_1 : Acc r b_1),
    hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry
Tactic: obtain rfl | ho := ho.eq_or_lt
Cleared hypotheses: o, ho_1, IH, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
b : α
hb : r b a
ho : o ≤ rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
inr :
  ∀ (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤ ha_1.rank (r := r))
    (IH :
      ∀ (y : α) (a_2 : r y a)
        (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ < ⋯.rank (r := r)),
        ∃ (b_1 : α) (hb_1 : Acc r b_1),
          hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯)
    (ho :
      rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤
        rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯),
    ∃ (b_1 : α) (hb_1 : Acc r b_1),
      hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have inr₁ : ∀ (ho : o < rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry),
  ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
Tactic: obtain rfl | ho := ho.eq_or_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
o : Ordinal.{u}
h : o ≤ rank r a
⊢ o ∈ Set.range (rank r)
have obtain : ∀ (b : α) (hb : Acc r b) (h : hb.rank (r := r) ≤ rank r a), hb.rank (r := r) ∈ Set.range (rank r)
Tactic: obtain ⟨b, hb, rfl⟩ := Acc.mem_range_rank_of_le (hwf.apply r a) h
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
⊢ rank r =
    (⇑((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u})
have h : ∀ (a : α),
  rank r a =
    ((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
letI letI₁ letI₂ :
  rank r =
    (⇑((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u})
⊢ rank r =
    (⇑((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u})
have h : ∀ (a : α),
  rank r a =
    ((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a
Tactic: classical
  letI := linearOrderOfSTO r
  ext a
  exact InitialSeg.eq (⟨(OrderEmbedding.ofStrictMono _ WellFoundedLT.rank_strictMono).ltEmbedding,
    fun a b h ↦ mem_range_rank_of_le h.le⟩) (Ordinal.typein r) a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
Goal:
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,
      ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a].TFAE
have tfae_1_to_2 : ∀ (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
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
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
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
have inl : ∀ (he : s ∩ Iic a = ∅), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
Tactic: rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
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
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
have inr : ∀ (hne : (s ∩ Iic a).Nonempty), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
Tactic: rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
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
have inr : a ∈ upperBounds (s ∩ Iic a)
Tactic: refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
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, a ∈ closure (s ∩ Iic a), (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].TFAE
have tfae_2_to_3 : ∀ (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
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
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 ∈ 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,
      ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a].TFAE
have tfae_3_to_4 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
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
⊢ ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = sSup t
have ht₂ : Small.{u, u + 1} (↑t : Type (u + 1))
Tactic: rw [bddAbove_iff_small] at ht₁
Cleared hypotheses: ht₁, tfae_1_to_2, tfae_2_to_3, tfae_3_to_4
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
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
have refine_1 : Nonempty.{u + 1} (Shrink.{u, u + 1} (↑t : Type (u + 1)))
Tactic: refine ⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
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)))
⊢ ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = sSup t
have 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
Tactic: refine ⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
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
⊢ ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = sSup t
have 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
Tactic: refine ⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
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 + 1} (Shrink.{u, u + 1} (↑t : Type (u + 1)))
have this : Nonempty.{u + 2} (↑t : Type (u + 1))
Tactic: have := ht₀.to_subtype
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
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 ∈ 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,
      ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a].TFAE
have 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
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']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
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, a ∈ closure (s ∩ Iic a), (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].TFAE
have tfae_5_to_1 : ∀ (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
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
have apply : (∃ (ι : 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: apply ((mem_closure_tfae a s).out 0 4).trans
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
have rw : a ∈ s ↔ a ∈ closure s
Tactic: rw [← mem_closure_iff_iSup, hs.closure_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
rw : a ∈ s ↔ a ∈ closure s
⊢ a ∈ s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
have rw₁ : a ∈ s ↔ a ∈ s
Tactic: rw [← mem_closure_iff_iSup, hs.closure_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔
    ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
      (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
have rw : (∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a) ↔
  ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
    (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
Tactic: rw [mem_closure_iff_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a) ↔
    ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
      (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
have mp : (∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a) →
  ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
    (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
mp :
  (∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a) →
    ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
      (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
⊢ (∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a) ↔
    ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
      (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
have mpr : (∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
    (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a) →
  ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔
    ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
      (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
have rw : a ∈ s ↔ a ∈ closure s
Tactic: rw [← mem_closure_iff_bsup, hs.closure_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
rw : a ∈ s ↔ a ∈ closure s
⊢ a ∈ s ↔
    ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
      (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
have rw₁ : a ∈ s ↔ a ∈ s
Tactic: rw [← mem_closure_iff_bsup, hs.closure_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s
have mpr : (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) → IsClosed s
Tactic: use fun hs ι hι f hf => (mem_iff_iSup_of_isClosed hs).2 ⟨ι, hι, f, hf, rfl⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) → IsClosed s
have mpr : (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) → closure s ⊆ s
Tactic: rw [← closure_subset_iff_isClosed]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s
x : Ordinal.{u}
hx : x ∈ closure s
⊢ x ∈ s
have mpr : ∀ (ι : Type u) (hι : Nonempty ι) (f : ι → Ordinal.{u}) (hf : ∀ (i : ι), f i ∈ s) (hx : ⨆ (i : ι), f i ∈ closure s),
  ⨆ (i : ι), f i ∈ s
Tactic: rcases mem_closure_iff_iSup.1 hx with ⟨ι, hι, f, hf, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
⊢ IsClosed s ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
have rw : (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) ↔
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
Tactic: rw [isClosed_iff_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
have refine_1 : ∀ (H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s)
  (o : Ordinal.{u}) (ho : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u})
  (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) (i : o.ToType), o.familyOfBFamily f i ∈ s
Tactic: refine ⟨fun H o ho f hf => H (nonempty_toType_iff.2 ho) _ ?_, fun H ι hι f hf => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
refine_1 :
  ∀ (H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s)
    (o : Ordinal.{u}) (ho : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u})
    (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) (i : o.ToType), o.familyOfBFamily f i ∈ s
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
have refine_2 : ∀
  (H :
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s)
  (ι : Type u) (hι : Nonempty ι) (f : ι → Ordinal.{u}) (hf : ∀ (i : ι), f i ∈ s), ⨆ (i : ι), f i ∈ s
Tactic: refine ⟨fun H o ho f hf => H (nonempty_toType_iff.2 ho) _ ?_, fun H ι hι f hf => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ (i : ι), f i ∈ s
have refine_2 : (type (α := ι) WellOrderingRel).bsup (bfamilyOfFamily fun (i : ι) ↦ f i) ∈ s
Tactic: rw [← bsup_eq_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ (type (α := ι) WellOrderingRel).bsup (bfamilyOfFamily fun (i : ι) ↦ f i) ∈ s
have refine_2 : ∀ (i : Ordinal.{u}) (hi : i < type (α := ι) WellOrderingRel), bfamilyOfFamily (fun (i : ι) ↦ f i) i hi ∈ s
Tactic: apply H (type_ne_zero_iff_nonempty.2 hι)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s) ↔ IsClosed s
have Hs : StrictMono (enumOrd s)
Tactic: have Hs := enumOrd_strictMono hs
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
⊢ IsNormal (enumOrd s) ↔ IsClosed s
have refine_1 : ∀ (h : IsNormal (enumOrd s)) {ι : Type u} (hι : Nonempty ι) (f : ι → Ordinal.{u}) (hf : ∀ (i : ι), f i ∈ s),
  ⨆ (i : ι), f i ∈ s
Tactic: refine
    ⟨fun h => isClosed_iff_iSup.2 fun {ι} hι f hf => ?_, fun h =>
      isNormal_iff.2 ⟨Hs, fun a ha o H => ?_⟩⟩