awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
tfae_5_to_1 :
  ∀ (a_1 : ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (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,
      ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
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
⊢ a ∈ closure s ↔ ∃ (ι : 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

Premises used: Ordinal.mem_closure_tfae, List.TFAE.out, Iff.trans, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ (ι : 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:
simp_rw [exists_prop]

Premises used: exists_prop
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
rw : a ∈ s ↔ a ∈ closure s
rw₁ rw₂ : a ∈ s ↔ a ∈ s
⊢ a ∈ s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a

Tactic:
rw [← mem_closure_iff_iSup, hs.closure_eq]

Premises used: IsClosed.closure_eq, Ordinal.mem_closure_iff_iSup
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
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
⊢ 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

Tactic:
rw [mem_closure_iff_iSup]

Premises used: Ordinal.mem_closure_iff_iSup
-- Module: Mathlib.SetTheory.Ordinal.Topology
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
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
⊢ (∃ (ι : 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
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
ι : Type u
w : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ type (α := ι) WellOrderingRel ≠ 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
ι : Type u
w : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f_1 : (a : Ordinal.{u}) → a < o → Ordinal.{u}),
    (∀ (i : Ordinal.{u}) (hi : i < o), f_1 i hi ∈ s) ∧ o.bsup f_1 = ⨆ (i : ι), f i

Tactic:
exact ⟨_, by simp, bfamilyOfFamily f, fun i hi ↦ hf .., bsup_eq_iSup f⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
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
⊢ Nonempty.{u + 1} o.ToType

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
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
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (f_1 : ι → Ordinal.{u}), (∀ (i : ι), f_1 i ∈ s) ∧ ⨆ (i : ι), f_1 i = o.bsup f

Tactic:
exact ⟨_, by simpa, familyOfBFamily _ f, fun i ↦ hf .., iSup_eq_bsup f⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
rw : a ∈ s ↔ a ∈ closure s
rw₁ rw₂ : a ∈ s ↔ a ∈ 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

Tactic:
rw [← mem_closure_iff_bsup, hs.closure_eq]

Premises used: Ordinal.mem_closure_iff_bsup, IsClosed.closure_eq
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
mpr : (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) → IsClosed s
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s

Tactic:
use fun hs ι hι f hf => (mem_iff_iSup_of_isClosed hs).2 ⟨ι, hι, f, hf, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Ordinal.mem_iff_iSup_of_isClosed, rfl
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
mpr : (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) → closure s ⊆ s
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s) → IsClosed s

Tactic:
rw [← closure_subset_iff_isClosed]

Premises used: closure_subset_iff_isClosed
-- Module: Mathlib.SetTheory.Ordinal.Topology
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
mpr :
  ∀ (ι : Type u) (hι : Nonempty ι) (f : ι → Ordinal.{u}) (hf : ∀ (i : ι), f i ∈ s) (hx : ⨆ (i : ι), f i ∈ closure s),
    ⨆ (i : ι), f i ∈ s
⊢ x ∈ s

Tactic:
rcases mem_closure_iff_iSup.1 hx with ⟨ι, hι, f, hf, rfl⟩

Premises used: Ordinal.mem_closure_iff_iSup, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
hx : ⨆ (i : ι), f i ∈ closure s
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
h hι f hf
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
hx : ⨆ (i : ι), f i ∈ closure s
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
exact h hι f hf
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
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
⊢ 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

Tactic:
rw [isClosed_iff_iSup]

Premises used: Ordinal.isClosed_iff_iSup
-- Module: Mathlib.SetTheory.Ordinal.Topology
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

Tactic:
⟨fun H o ho f hf => H (nonempty_toType_iff.2 ho) _ ?_, fun H ι hι f hf => ?_⟩

Premises used: Iff.mpr, Ordinal.familyOfBFamily, Ordinal.nonempty_toType_iff, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Topology
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
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
⊢ (∀ {ι : 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:
refine ⟨fun H o ho f hf => H (nonempty_toType_iff.2 ho) _ ?_, fun H ι hι f hf => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
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:
fun i => hf _ _

Premises used: Set.Mem, Ordinal.familyOfBFamily, PrincipalSeg.toRelEmbedding, LT.lt, Ordinal.familyOfBFamily', DFunLike.coe, Ordinal.type_toType, Ordinal.typein, Ordinal.familyOfBFamily'._proof_1
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
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:
exact fun i => hf _ _
-- Module: Mathlib.SetTheory.Ordinal.Topology
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
refine_2 : (type (α := ι) WellOrderingRel).bsup (bfamilyOfFamily fun (i : ι) ↦ f i) ∈ s
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
rw [← bsup_eq_iSup]

Premises used: Ordinal.bsup_eq_iSup
-- Module: Mathlib.SetTheory.Ordinal.Topology
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
refine_2 : ∀ (i : Ordinal.{u}) (hi : i < type (α := ι) WellOrderingRel), bfamilyOfFamily (fun (i : ι) ↦ f i) i hi ∈ s
⊢ (type (α := ι) WellOrderingRel).bsup (bfamilyOfFamily fun (i : ι) ↦ f i) ∈ s

Tactic:
apply H (type_ne_zero_iff_nonempty.2 hι)

Premises used: Iff.mpr, Ordinal.type_ne_zero_iff_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Topology
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 : Ordinal.{u}) (hi : i < type (α := ι) WellOrderingRel), bfamilyOfFamily (fun (i : ι) ↦ f i) i hi ∈ s

Tactic:
fun i hi => hf _

Premises used: Ordinal.bfamilyOfFamily', Ordinal.bfamilyOfFamily, Set.Mem, Subtype.mk, Ordinal.enum, DFunLike.coe, WellOrderingRel
-- Module: Mathlib.SetTheory.Ordinal.Topology
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 : Ordinal.{u}) (hi : i < type (α := ι) WellOrderingRel), bfamilyOfFamily (fun (i : ι) ↦ f i) i hi ∈ s

Tactic:
exact fun i hi => hf _
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : a ∈ frontier s
⊢ IsSuccLimit a

Tactic:
SuccOrder.isSuccLimit_of_mem_frontier ha

Premises used: SuccOrder.isSuccLimit_of_mem_frontier
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono (enumOrd s)

Tactic:
have Hs := enumOrd_strictMono hs
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
⊢ IsNormal (enumOrd s) ↔ IsClosed s

Tactic:
⟨fun h => isClosed_iff_iSup.2 fun {ι} hι f hf => ?_, fun h =>
      isNormal_iff.2 ⟨Hs, fun a ha o H => ?_⟩⟩

Premises used: Iff.mpr, And.intro, Iff.intro, Order.isNormal_iff, Ordinal.isClosed_iff_iSup
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
refine_1 :
  ∀ (h : IsNormal (enumOrd s)) {ι : Type u} (hι : Nonempty ι) (f : ι → Ordinal.{u}) (hf : ∀ (i : ι), f i ∈ s),
    ⨆ (i : ι), f i ∈ s
refine_2 :
  ∀ (h : IsClosed s) (a : Ordinal.{u}) (ha : IsSuccLimit a) (o : Ordinal.{u}) (H : ∀ b < a, enumOrd s b ≤ o),
    enumOrd s a ≤ o
⊢ IsNormal (enumOrd s) ↔ IsClosed s

Tactic:
refine
    ⟨fun h => isClosed_iff_iSup.2 fun {ι} hι f hf => ?_, fun h =>
      isNormal_iff.2 ⟨Hs, fun a ha o H => ?_⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
this : enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i
rw : enumOrd s (⨆ (i : ι), g i) ∈ s
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
rw [← this]
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
this : enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i
⊢ enumOrd s (⨆ (i : ι), g i) ∈ s

Tactic:
enumOrd_mem hs _

Premises used: Ordinal.enumOrd_mem
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
this : enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i
⊢ enumOrd s (⨆ (i : ι), g i) ∈ s

Tactic:
exact enumOrd_mem hs _

Premises used: Ordinal.enumOrd_mem
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
refine_1 : enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
      rw [← this]
      exact enumOrd_mem hs _
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
refine_1 : Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : ι), enumOrd s (g i)) (⨆ (i : ι), f i)
⊢ enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i

Tactic:
rw [h.map_iSup bddAbove_of_small]

Premises used: Ordinal.bddAbove_of_small, Order.IsNormal.map_iSup
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
refine_1 : Eq.{u + 2} (α := ι → Ordinal.{u}) (fun (i : ι) ↦ enumOrd s (g i)) fun (i : ι) ↦ f i
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : ι), enumOrd s (g i)) (⨆ (i : ι), f i)

Tactic:
congr
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
refine_1 : ∀ (x : ι), enumOrd s (g x) = f x
⊢ Eq.{u + 2} (α := ι → Ordinal.{u}) (fun (i : ι) ↦ enumOrd s (g i)) fun (i : ι) ↦ f i

Tactic:
ext x
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
x : ι
refine_1 refine_1₁ : (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f x) ⋯) : Ordinal.{u}) = f x
⊢ (↑((enumOrdOrderIso s hs : (a : Ordinal.{u}) → (↑s : Type (u + 1))) (g x)) : Ordinal.{u}) = f x

Tactic:
rw [OrderIso.apply_symm_apply]

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
⊢ sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)

Tactic:
have := csSup_mem_closure (ha.nonempty_Iio.image (enumOrd s)) bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
refine_2 : enumOrd s '' Set.Iio a ⊆ s
refine_2₁ : ∀ (this : sSup (enumOrd s '' Set.Iio a) ∈ s), enumOrd s a ≤ o
⊢ enumOrd s a ≤ o

Tactic:
have := h.closure_eq ▸ closure_mono (t := s) ?_ this
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
refine_2 : Set.range (enumOrd s) = s
⊢ enumOrd s '' Set.Iio a ⊆ s

Tactic:
apply (Set.image_subset_range ..).trans_eq

Premises used: LE.le.trans_eq, Set.image_subset_range
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
refine_2 refine_2₁ : s = s
⊢ Set.range (enumOrd s) = s

Tactic:
rw [range_enumOrd hs]

Premises used: Ordinal.range_enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
refine_2 : sSup (enumOrd s '' Set.Iio a) ≤ o
apply : ∀ b < a, enumOrd s b < sSup (enumOrd s '' Set.Iio a)
⊢ enumOrd s a ≤ o

Tactic:
apply (enumOrd_le_of_forall_lt this _).trans

Premises used: Ordinal.enumOrd_le_of_forall_lt, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
refine_2 : o ∈ upperBounds (enumOrd s '' Set.Iio a)
⊢ sSup (enumOrd s '' Set.Iio a) ≤ o

Tactic:
apply csSup_le'

Premises used: csSup_le'
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ o ∈ upperBounds (enumOrd s '' Set.Iio a)

Tactic:
grind [upperBounds]

Premises used: upperBounds
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ ∀ b < a, enumOrd s b < sSup (enumOrd s '' Set.Iio a)

Tactic:
fun b hb ↦ (enumOrd_strictMono hs (lt_add_one b)).trans_le <|
          le_csSup bddAbove_of_small <| Set.mem_image_of_mem _ (ha.add_one_lt hb)

Premises used: lt_add_one, Order.IsSuccLimit.add_one_lt, Ordinal.enumOrd, Ordinal.bddAbove_of_small, Set.mem_image_of_mem, LT.lt.trans_le, le_csSup, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ ∀ b < a, enumOrd s b < sSup (enumOrd s '' Set.Iio a)

Tactic:
exact fun b hb ↦ (enumOrd_strictMono hs (lt_add_one b)).trans_le <|
          le_csSup bddAbove_of_small <| Set.mem_image_of_mem _ (ha.add_one_lt hb)

Premises used: lt_add_one, Order.IsSuccLimit.add_one_lt, Ordinal.enumOrd, Ordinal.bddAbove_of_small, Set.mem_image_of_mem, LT.lt.trans_le, le_csSup, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
mp : AccPt o (𝓟 S) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
mpr : (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → AccPt o (𝓟 S)
⊢ AccPt o (𝓟 S) ↔ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
mp : (∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ AccPt o (𝓟 S) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
rw [accPt_iff_nhds]

Premises used: accPt_iff_nhds
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
mp : ¬o = 0
mp₁ : ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
S : Set Ordinal.{u_1}
h : ∀ (U : Set Ordinal.{u_1}), Membership.mem (γ := Filter Ordinal.{u_1}) (𝓝 0) U → ∃ y ∈ U ∩ S, y ≠ 0
mp : ∀ (x : Ordinal.{u_1}) (hx : x ∈ Iio 1 ∩ S ∧ x ≠ 0), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := h (Iio 1) (Iio_mem_nhds zero_lt_one)

Premises used: Iio_mem_nhds, zero_lt_one, OfNat.ofNat, Set.Iio