[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ IsOpen {a} ↔ ¬IsLimit a
[PROOFSTEP]
refine' ⟨fun h ⟨h₀, hsucc⟩ => _, fun ha => _⟩
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal.{u}), a_1 < a → succ a_1 < a
⊢ False
[PROOFSTEP]
obtain ⟨b, c, hbc, hbc'⟩ :=
  (mem_nhds_iff_exists_Ioo_subset' ⟨0, Ordinal.pos_iff_ne_zero.2 h₀⟩ ⟨_, lt_succ a⟩).1 (h.mem_nhds rfl)
[GOAL]
case refine'_1.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal.{u}), a_1 < a → succ a_1 < a
b c : Ordinal.{u}
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
⊢ False
[PROOFSTEP]
have hba := hsucc b hbc.1
[GOAL]
case refine'_1.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal.{u}), a_1 < a → succ a_1 < a
b c : Ordinal.{u}
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
hba : succ b < a
⊢ False
[PROOFSTEP]
exact hba.ne (hbc' ⟨lt_succ b, hba.trans hbc.2⟩)
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : ¬IsLimit a
⊢ IsOpen {a}
[PROOFSTEP]
rcases zero_or_succ_or_limit a with (rfl | ⟨b, rfl⟩ | ha')
[GOAL]
case refine'_2.inl
s : Set Ordinal.{u}
ha : ¬IsLimit 0
⊢ IsOpen {0}
[PROOFSTEP]
rw [← bot_eq_zero, ← Set.Iic_bot, ← Iio_succ]
[GOAL]
case refine'_2.inl
s : Set Ordinal.{u}
ha : ¬IsLimit 0
⊢ IsOpen (Set.Iio (succ ⊥))
[PROOFSTEP]
exact isOpen_Iio
[GOAL]
case refine'_2.inr.inl.intro
s : Set Ordinal.{u}
b : Ordinal.{u}
ha : ¬IsLimit (succ b)
⊢ IsOpen {succ b}
[PROOFSTEP]
rw [← Set.Icc_self, Icc_succ_left, ← Ioo_succ_right]
[GOAL]
case refine'_2.inr.inl.intro
s : Set Ordinal.{u}
b : Ordinal.{u}
ha : ¬IsLimit (succ b)
⊢ IsOpen (Set.Ioo b (succ (succ b)))
[PROOFSTEP]
exact isOpen_Ioo
[GOAL]
case refine'_2.inr.inr
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : ¬IsLimit a
ha' : IsLimit a
⊢ IsOpen {a}
[PROOFSTEP]
exact (ha ha').elim
[GOAL]
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
a : Ordinal.{u_1}
⊢ 𝓝[Set.Iio a] a = 𝓝[{a}ᶜ] a
[PROOFSTEP]
rw [← nhds_left'_sup_nhds_right', nhds_right', sup_bot_eq]
  -- todo: generalize to a `SuccOrder`
[GOAL]
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
a : Ordinal.{u_1}
⊢ 𝓝[Set.Iic a] a = 𝓝 a
[PROOFSTEP]
rw [← nhds_left_sup_nhds_right', nhds_right', sup_bot_eq]
  -- todo: generalize to a `SuccOrder`
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ IsOpen s ↔ ∀ (o : Ordinal.{u}), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
[PROOFSTEP]
refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho => ?_
[GOAL]
s : Set Ordinal.{u}
a o : Ordinal.{u}
ho : o ∈ s
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
[PROOFSTEP]
by_cases ho' : IsLimit o
[GOAL]
case pos
s : Set Ordinal.{u}
a o : Ordinal.{u}
ho : o ∈ s
ho' : IsLimit o
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
[PROOFSTEP]
simp only [(nhdsBasis_Ioc ho'.1).mem_iff, ho', true_implies]
[GOAL]
case pos
s : Set Ordinal.{u}
a o : Ordinal.{u}
ho : o ∈ s
ho' : IsLimit o
⊢ (∃ i, i < o ∧ Set.Ioc i o ⊆ s) ↔ ∃ a, a < o ∧ Set.Ioo a o ⊆ s
[PROOFSTEP]
refine exists_congr fun a => and_congr_right fun ha => ?_
[GOAL]
case pos
s : Set Ordinal.{u}
a✝ o : Ordinal.{u}
ho : o ∈ s
ho' : IsLimit o
a : Ordinal.{u}
ha : a < o
⊢ Set.Ioc a o ⊆ s ↔ Set.Ioo a o ⊆ s
[PROOFSTEP]
simp only [← Set.Ioo_insert_right ha, Set.insert_subset_iff, ho, true_and]
[GOAL]
case neg
s : Set Ordinal.{u}
a o : Ordinal.{u}
ho : o ∈ s
ho' : ¬IsLimit o
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
[PROOFSTEP]
simp [nhds_eq_pure.2 ho', ho, ho']
[GOAL]
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ a ∈ closure s → a ∈ closure (s ∩ Iic a)
[PROOFSTEP]
simp only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter', nhds_left_eq_nhds]
[GOAL]
case tfae_1_to_2
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ Filter.NeBot (𝓝[s] a) → Filter.NeBot (𝓝 a ⊓ Filter.principal s)
[PROOFSTEP]
exact id
[GOAL]
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
⊢ a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
[PROOFSTEP]
intro h
[GOAL]
case tfae_2_to_3
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
[PROOFSTEP]
cases' (s ∩ Iic a).eq_empty_or_nonempty with he hne
[GOAL]
case tfae_2_to_3.inl
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
he : s ∩ Iic a = ∅
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
[PROOFSTEP]
simp [he] at h
[GOAL]
case tfae_2_to_3.inr
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
hne : Set.Nonempty (s ∩ Iic a)
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
[PROOFSTEP]
refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
[GOAL]
case tfae_2_to_3.inr
s✝ : Set Ordinal.{u}
a✝ a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
hne : Set.Nonempty (s ∩ Iic a)
⊢ a ∈ upperBounds (s ∩ Iic a)
[PROOFSTEP]
exact fun x hx => hx.2
[GOAL]
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
[PROOFSTEP]
tfae_have 3 → 4
[GOAL]
case tfae_3_to_4
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
[PROOFSTEP]
exact fun h => ⟨_, inter_subset_left _ _, h.1, bddAbove_Iic.mono (inter_subset_right _ _), h.2⟩
[GOAL]
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
[PROOFSTEP]
tfae_have 4 → 5
[GOAL]
case tfae_4_to_5
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
⊢ (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
[PROOFSTEP]
rintro ⟨t, hts, hne, hbdd, rfl⟩
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
[PROOFSTEP]
have hlub : IsLUB t (sSup t) := isLUB_csSup hne hbdd
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
[PROOFSTEP]
let ⟨y, hyt⟩ := hne
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal.{u}
hyt : y ∈ t
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
[PROOFSTEP]
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 _))
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal.{u}
hyt : y ∈ t
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
[PROOFSTEP]
refine ⟨succ (sSup t), succ_ne_zero _, fun x _ => if x ∈ t then x else y, fun x _ => ?_, ?_⟩
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro.refine_1
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ 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
[PROOFSTEP]
simp only
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro.refine_1
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ 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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ 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)
h : x ∈ t
⊢ x ∈ s
[PROOFSTEP]
exact hts ‹_›
[GOAL]
case neg
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ 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)
h : ¬x ∈ t
⊢ y ∈ s
[PROOFSTEP]
exact hts ‹_›
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro.refine_2
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal.{u}
hyt : y ∈ t
⊢ (bsup (succ (sSup t)) fun x x_1 => if x ∈ t then x else y) = sSup t
[PROOFSTEP]
refine le_antisymm (bsup_le fun x _ => ?_) (csSup_le hne fun x hx => ?_)
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro.refine_2.refine_1
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ 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) ≤ sSup t
[PROOFSTEP]
split_ifs
[GOAL]
case pos
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ 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)
h✝ : x ∈ t
⊢ x ≤ sSup t
[PROOFSTEP]
exact hlub.1 ‹_›
[GOAL]
case neg
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ 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)
h✝ : ¬x ∈ t
⊢ y ≤ sSup t
[PROOFSTEP]
exact hlub.1 ‹_›
[GOAL]
case tfae_4_to_5.intro.intro.intro.intro.refine_2.refine_2
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s t : Set Ordinal.{u}
hts : t ⊆ s
hne : Set.Nonempty t
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)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal.{u}
hyt : y ∈ t
x : Ordinal.{u}
hx : x ∈ t
⊢ x ≤ bsup (succ (sSup t)) fun x x_1 => if x ∈ t then x else y
[PROOFSTEP]
refine (if_pos hx).symm.trans_le (le_bsup _ _ <| (hlub.1 hx).trans_lt (lt_succ _))
[GOAL]
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
[PROOFSTEP]
tfae_have 5 → 6
[GOAL]
case tfae_5_to_6
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
⊢ (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
[PROOFSTEP]
rintro ⟨o, h₀, f, hfs, rfl⟩
[GOAL]
case tfae_5_to_6.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
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 : bsup o f ∈ closure s → bsup o f ∈ closure (s ∩ Iic (bsup o f))
tfae_2_to_3 :
  bsup o f ∈ closure (s ∩ Iic (bsup o f)) → Set.Nonempty (s ∩ Iic (bsup o f)) ∧ sSup (s ∩ Iic (bsup o f)) = bsup o f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (bsup o f)) ∧ sSup (s ∩ Iic (bsup o f)) = bsup o f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = bsup o f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = bsup o f) →
    ∃ o_1, o_1 ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o_1), f_1 x hx ∈ s) ∧ bsup o_1 f_1 = bsup o f
⊢ ∃ ι, Nonempty ι ∧ ∃ f_1, (∀ (i : ι), f_1 i ∈ s) ∧ sup f_1 = bsup o f
[PROOFSTEP]
exact ⟨_, out_nonempty_iff_ne_zero.2 h₀, familyOfBFamily o f, fun _ => hfs _ _, rfl⟩
[GOAL]
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
[PROOFSTEP]
tfae_have 6 → 1
[GOAL]
case tfae_6_to_1
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) → a ∈ closure s
[PROOFSTEP]
rintro ⟨ι, hne, f, hfs, rfl⟩
[GOAL]
case tfae_6_to_1.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s : Set Ordinal.{u}
ι : Type u
hne : Nonempty ι
f : ι → Ordinal.{u}
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : sup f ∈ closure s → sup f ∈ closure (s ∩ Iic (sup f))
tfae_2_to_3 : sup f ∈ closure (s ∩ Iic (sup f)) → Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ sup f_1 = sup f
⊢ sup f ∈ closure s
[PROOFSTEP]
rw [sup, iSup]
[GOAL]
case tfae_6_to_1.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
s : Set Ordinal.{u}
ι : Type u
hne : Nonempty ι
f : ι → Ordinal.{u}
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : sup f ∈ closure s → sup f ∈ closure (s ∩ Iic (sup f))
tfae_2_to_3 : sup f ∈ closure (s ∩ Iic (sup f)) → Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal.{u}) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ sup f_1 = sup f
⊢ sSup (Set.range f) ∈ closure s
[PROOFSTEP]
exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f) (bddAbove_range.{u, u} f)
[GOAL]
s✝ : Set Ordinal.{u}
a✝ 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) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
tfae_6_to_1 : (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) → a ∈ closure s
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
[PROOFSTEP]
tfae_finish
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) ↔ ∃ ι x f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
[PROOFSTEP]
simp only [exists_prop]
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔ ∃ ι _hι f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
[PROOFSTEP]
rw [← mem_closure_iff_sup, hs.closure_eq]
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) ↔
    ∃ o _ho f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ bsup o f = a
[PROOFSTEP]
simp only [exists_prop]
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔ ∃ o _ho f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ bsup o f = a
[PROOFSTEP]
rw [← mem_closure_iff_bsup, hs.closure_eq]
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s
[PROOFSTEP]
use fun hs ι hι f hf => (mem_closed_iff_sup hs).2 ⟨ι, hι, f, hf, rfl⟩
[GOAL]
case mpr
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s) → IsClosed s
[PROOFSTEP]
rw [← closure_subset_iff_isClosed]
[GOAL]
case mpr
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s) → closure s ⊆ s
[PROOFSTEP]
intro h x hx
[GOAL]
case mpr
s : Set Ordinal.{u}
a : Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s
x : Ordinal.{u}
hx : x ∈ closure s
⊢ x ∈ s
[PROOFSTEP]
rcases mem_closure_iff_sup.1 hx with ⟨ι, hι, f, hf, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
hx : sup f ∈ closure s
⊢ sup f ∈ s
[PROOFSTEP]
exact h hι f hf
[GOAL]
s : Set Ordinal.{u}
a : 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) → bsup o f ∈ s
[PROOFSTEP]
rw [isClosed_iff_sup]
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s) ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
[PROOFSTEP]
refine' ⟨fun H o ho f hf => H (out_nonempty_iff_ne_zero.2 ho) _ _, fun H ι hι f hf => _⟩
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ 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 : (Quotient.out o).α), familyOfBFamily o f i ∈ s
[PROOFSTEP]
exact fun i => hf _ _
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a : 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) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ sup f ∈ s
[PROOFSTEP]
rw [← bsup_eq_sup]
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a : 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) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ bsup (type WellOrderingRel) (bfamilyOfFamily f) ∈ s
[PROOFSTEP]
apply H (type_ne_zero_iff_nonempty.2 hι)
[GOAL]
case refine'_2.a
s : Set Ordinal.{u}
a : 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) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ∀ (i : Ordinal.{u}) (hi : i < type WellOrderingRel), bfamilyOfFamily f i hi ∈ s
[PROOFSTEP]
exact fun i hi => hf _
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : a ∈ frontier s
⊢ IsLimit a
[PROOFSTEP]
simp only [frontier_eq_closure_inter_closure, Set.mem_inter_iff, mem_closure_iff] at ha
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
⊢ IsLimit a
[PROOFSTEP]
by_contra h
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : ¬IsLimit a
⊢ False
[PROOFSTEP]
rw [← isOpen_singleton_iff] at h
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
⊢ False
[PROOFSTEP]
rcases ha.1 _ h rfl with ⟨b, hb, hb'⟩
[GOAL]
case intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal.{u}
hb : b ∈ {a}
hb' : b ∈ s
⊢ False
[PROOFSTEP]
rcases ha.2 _ h rfl with ⟨c, hc, hc'⟩
[GOAL]
case intro.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal.{u}
hb : b ∈ {a}
hb' : b ∈ s
c : Ordinal.{u}
hc : c ∈ {a}
hc' : c ∈ sᶜ
⊢ False
[PROOFSTEP]
rw [Set.mem_singleton_iff] at *
[GOAL]
case intro.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal.{u}
hb : b = a
hb' : b ∈ s
c : Ordinal.{u}
hc : c = a
hc' : c ∈ sᶜ
⊢ False
[PROOFSTEP]
subst hb
[GOAL]
case intro.intro.intro.intro
s : Set Ordinal.{u}
b : Ordinal.{u}
hb' : b ∈ s
c : Ordinal.{u}
hc' : c ∈ sᶜ
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → b ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → b ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {b}
hc : c = b
⊢ False
[PROOFSTEP]
subst hc
[GOAL]
case intro.intro.intro.intro
s : Set Ordinal.{u}
c : Ordinal.{u}
hc' : c ∈ sᶜ
hb' : c ∈ s
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → c ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → c ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {c}
⊢ False
[PROOFSTEP]
exact hc' hb'
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
⊢ IsNormal f ↔ StrictMono f ∧ Continuous f
[PROOFSTEP]
refine' ⟨fun h => ⟨h.strictMono, _⟩, _⟩
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
⊢ Continuous f
[PROOFSTEP]
rw [continuous_def]
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
⊢ ∀ (s : Set Ordinal.{u}), IsOpen s → IsOpen (f ⁻¹' s)
[PROOFSTEP]
intro s hs
[GOAL]
case refine'_1
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)
[PROOFSTEP]
rw [isOpen_iff] at *
[GOAL]
case refine'_1
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ (o : Ordinal.{u}), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
⊢ ∀ (o : Ordinal.{u}), o ∈ f ⁻¹' s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
[PROOFSTEP]
intro o ho ho'
[GOAL]
case refine'_1
s✝ : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ (o : Ordinal.{u}), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
[PROOFSTEP]
rcases hs _ ho (h.isLimit ho') with ⟨a, ha, has⟩
[GOAL]
case refine'_1.intro.intro
s✝ : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ (o : Ordinal.{u}), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal.{u}
ha : a < f o
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
[PROOFSTEP]
rw [← IsNormal.bsup_eq.{u, u} h ho', lt_bsup] at ha
[GOAL]
case refine'_1.intro.intro
s✝ : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ (o : Ordinal.{u}), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal.{u}
ha : ∃ i hi, a < f i
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
[PROOFSTEP]
rcases ha with ⟨b, hb, hab⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
s✝ : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ (o : Ordinal.{u}), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal.{u}
has : Set.Ioo a (f o) ⊆ s
b : Ordinal.{u}
hb : b < o
hab : a < f b
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
[PROOFSTEP]
exact ⟨b, hb, fun c hc => Set.mem_preimage.2 (has ⟨hab.trans (h.strictMono hc.1), h.strictMono hc.2⟩)⟩
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
⊢ StrictMono f ∧ Continuous f → IsNormal f
[PROOFSTEP]
rw [isNormal_iff_strictMono_limit]
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
⊢ StrictMono f ∧ Continuous f →
    StrictMono f ∧
      ∀ (o : Ordinal.{u}), IsLimit o → ∀ (a : Ordinal.{u}), (∀ (b : Ordinal.{u}), b < o → f b ≤ a) → f o ≤ a
[PROOFSTEP]
rintro ⟨h, h'⟩
[GOAL]
case refine'_2.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : StrictMono f
h' : Continuous f
⊢ StrictMono f ∧ ∀ (o : Ordinal.{u}), IsLimit o → ∀ (a : Ordinal.{u}), (∀ (b : Ordinal.{u}), b < o → f b ≤ a) → f o ≤ a
[PROOFSTEP]
refine' ⟨h, fun o ho a h => _⟩
[GOAL]
case refine'_2.intro
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : IsLimit o
a : Ordinal.{u}
h : ∀ (b : Ordinal.{u}), b < o → f b ≤ a
⊢ f o ≤ a
[PROOFSTEP]
suffices : o ∈ f ⁻¹' Set.Iic a
[GOAL]
case refine'_2.intro
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : IsLimit o
a : Ordinal.{u}
h : ∀ (b : Ordinal.{u}), b < o → f b ≤ a
this : o ∈ f ⁻¹' Set.Iic a
⊢ f o ≤ a
case this
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : IsLimit o
a : Ordinal.{u}
h : ∀ (b : Ordinal.{u}), b < o → f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a
[PROOFSTEP]
exact Set.mem_preimage.1 this
[GOAL]
case this
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : IsLimit o
a : Ordinal.{u}
h : ∀ (b : Ordinal.{u}), b < o → f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a
[PROOFSTEP]
rw [mem_closed_iff_sup (IsClosed.preimage h' (@isClosed_Iic _ _ _ _ a))]
[GOAL]
case this
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : IsLimit o
a : Ordinal.{u}
h : ∀ (b : Ordinal.{u}), b < o → f b ≤ a
⊢ ∃ ι _hι f_1, (∀ (i : ι), f_1 i ∈ f ⁻¹' Set.Iic a) ∧ sup f_1 = o
[PROOFSTEP]
exact ⟨_, out_nonempty_iff_ne_zero.2 ho.1, typein (· < ·), fun i => h _ (typein_lt_self i), sup_typein_limit ho.2⟩
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
⊢ IsNormal (enumOrd s) ↔ IsClosed s
[PROOFSTEP]
have Hs := enumOrd_strictMono hs
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
⊢ IsNormal (enumOrd s) ↔ IsClosed s
[PROOFSTEP]
refine'
  ⟨fun h => isClosed_iff_sup.2 fun {ι} hι f hf => _, fun h =>
    (isNormal_iff_strictMono_limit _).2 ⟨Hs, fun a ha o H => _⟩⟩
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ sup f ∈ s
[PROOFSTEP]
let g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso hs).symm ⟨_, hf i⟩
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ sup f ∈ s
[PROOFSTEP]
suffices enumOrd s (sup.{u, u} g) = sup.{u, u} f by
  rw [← this]
  exact enumOrd_mem hs _
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
this : enumOrd s (sup g) = sup f
⊢ sup f ∈ s
[PROOFSTEP]
rw [← this]
[GOAL]
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
this : enumOrd s (sup g) = sup f
⊢ enumOrd s (sup g) ∈ s
[PROOFSTEP]
exact enumOrd_mem hs _
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ enumOrd s (sup g) = sup f
[PROOFSTEP]
rw [@IsNormal.sup.{u, u, u} _ h ι g hι]
[GOAL]
case refine'_1
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ sup (enumOrd s ∘ g) = sup f
[PROOFSTEP]
congr
[GOAL]
case refine'_1.e_f
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ enumOrd s ∘ g = f
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.e_f.h
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
x : ι
⊢ (enumOrd s ∘ g) x = f x
[PROOFSTEP]
change ((enumOrdOrderIso hs) _).val = f x
[GOAL]
case refine'_1.e_f.h
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) 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 => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
x : ι
⊢ ↑(↑(enumOrdOrderIso hs) (g x)) = f x
[PROOFSTEP]
rw [OrderIso.apply_symm_apply]
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ o
[PROOFSTEP]
rw [isClosed_iff_bsup] at h
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ o
[PROOFSTEP]
suffices : enumOrd s a ≤ bsup.{u, u} a fun b (_ : b < a) => enumOrd s b
[GOAL]
case refine'_2
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
this : enumOrd s a ≤ bsup a fun b x => enumOrd s b
⊢ enumOrd s a ≤ o
case this
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
[PROOFSTEP]
exact this.trans (bsup_le H)
[GOAL]
case this
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
[PROOFSTEP]
cases' enumOrd_surjective hs _ (h ha.1 (fun b _ => enumOrd s b) fun b _ => enumOrd_mem hs b) with b hb
[GOAL]
case this.intro
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
[PROOFSTEP]
rw [← hb]
[GOAL]
case this.intro
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ enumOrd s a ≤ enumOrd s b
[PROOFSTEP]
apply Hs.monotone
[GOAL]
case this.intro.a
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ a ≤ b
[PROOFSTEP]
by_contra' hba
[GOAL]
case this.intro.a
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = bsup a fun b x => enumOrd s b
hba : b < a
⊢ False
[PROOFSTEP]
apply (Hs (lt_succ b)).not_le
[GOAL]
case this.intro.a
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = bsup a fun b x => enumOrd s b
hba : b < a
⊢ enumOrd s (succ b) ≤ enumOrd s b
[PROOFSTEP]
rw [hb]
[GOAL]
case this.intro.a
s : Set Ordinal.{u}
a✝ : Ordinal.{u}
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal.{u}
ha : IsLimit a
o : Ordinal.{u}
H : ∀ (b : Ordinal.{u}), b < a → enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = bsup a fun b x => enumOrd s b
hba : b < a
⊢ enumOrd s (succ b) ≤ bsup a fun b x => enumOrd s b
[PROOFSTEP]
exact le_bsup.{u, u} _ _ (ha.2 _ hba)