case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
⊢ enumOrd S (sSup {a | enumOrd S a ≤ s}) ≤ s

case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
⊢ s ≤ enumOrd S (sSup {a | enumOrd S a ≤ s})
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
⊢ enumOrd S (sSup {a | enumOrd S a ≤ s}) = s
apply le_antisymm
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
⊢ sInf (S ∩ {b | ∀ (c : Ordinal), c < sSup {a | enumOrd S a ≤ s} → enumOrd S c < b}) ≤ s
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
⊢ enumOrd S (sSup {a | enumOrd S a ≤ s}) ≤ s
rw [enumOrd_def]
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
⊢ enumOrd S a < s
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
⊢ sInf (S ∩ {b | ∀ (c : Ordinal), c < sSup {a | enumOrd S a ≤ s} → enumOrd S c < b}) ≤ s
refine' csInf_le' ⟨hs, fun a ha => _⟩
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
this : enumOrd S 0 ≤ s
⊢ enumOrd S a < s
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
⊢ enumOrd S a < s
have : enumOrd S 0 ≤ s := by
  rw [enumOrd_zero]
  exact csInf_le' hs
case a.intro.intro
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
this : enumOrd S 0 ≤ s
b : Ordinal
hb : b ∈ {a | enumOrd S a ≤ s}
hab : a < b
⊢ enumOrd S a < s
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
this : enumOrd S 0 ≤ s
⊢ enumOrd S a < s
rcases flip exists_lt_of_lt_csSup ha ⟨0, this⟩ with ⟨b, hb, hab⟩
no goals
case a.intro.intro
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
this : enumOrd S 0 ≤ s
b : Ordinal
hb : b ∈ {a | enumOrd S a ≤ s}
hab : a < b
⊢ enumOrd S a < s
exact (enumOrd_strictMono hS hab).trans_le hb
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
⊢ sInf S ≤ s
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
⊢ enumOrd S 0 ≤ s
rw [enumOrd_zero]
no goals
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
a : Ordinal
ha : a < sSup {a | enumOrd S a ≤ s}
⊢ sInf S ≤ s
exact csInf_le' hs
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
h : enumOrd S (sSup {a | enumOrd S a ≤ s}) < s
⊢ False
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
⊢ s ≤ enumOrd S (sSup {a | enumOrd S a ≤ s})
by_contra' h
no goals
case a
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
s : Ordinal
hs : s ∈ S
h : enumOrd S (sSup {a | enumOrd S a ≤ s}) < s
⊢ False
exact
  (le_csSup ⟨s, fun a => (lt_wf.self_le_of_strictMono (enumOrd_strictMono hS) a).trans⟩
        (enumOrd_succ_le hS hs h)).not_lt
    (lt_succ _)