s : Set Ordinal
a : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
⊢ IsNormal (enumOrd s) ↔ IsClosed s
s : Set Ordinal
a : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
⊢ IsNormal (enumOrd s) ↔ IsClosed s
have Hs := enumOrd_strictMono hs
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
⊢ sup f ∈ s

case refine'_2
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ o
s : Set Ordinal
a : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
⊢ IsNormal (enumOrd s) ↔ IsClosed s
refine'
  ⟨fun h => isClosed_iff_sup.2 fun {ι} hι f hf => _, fun h =>
    (isNormal_iff_strictMono_limit _).2 ⟨Hs, fun a ha o H => _⟩⟩
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ sup f ∈ s
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
⊢ sup f ∈ s
let g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso hs).symm ⟨_, hf i⟩
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ enumOrd s (sup g) = sup f
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ sup f ∈ s
suffices enumOrd s (sup.{u, u} g) = sup.{u, u} f by
  rw [← this]
  exact enumOrd_mem hs _
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ sup (enumOrd s ∘ g) = sup f
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ enumOrd s (sup g) = sup f
rw [@IsNormal.sup.{u, u, u} _ h ι g hι]
case refine'_1.e_f
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ enumOrd s ∘ g = f
case refine'_1
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ sup (enumOrd s ∘ g) = sup f
congr
case refine'_1.e_f.h
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
x : ι
⊢ (enumOrd s ∘ g) x = f x
case refine'_1.e_f
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
⊢ enumOrd s ∘ g = f
ext x
case refine'_1.e_f.h
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
x : ι
⊢ ↑(↑(enumOrdOrderIso hs) (g x)) = f x
case refine'_1.e_f.h
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
x : ι
⊢ (enumOrd s ∘ g) x = f x
change ((enumOrdOrderIso hs) _).val = f x
no goals
case refine'_1.e_f.h
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
x : ι
⊢ ↑(↑(enumOrdOrderIso hs) (g x)) = f x
rw [OrderIso.apply_symm_apply]
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := 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
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := fun i => ↑(OrderIso.symm (enumOrdOrderIso hs)) { val := f i, property := (_ : f i ∈ s) }
this : enumOrd s (sup g) = sup f
⊢ sup f ∈ s
rw [← this]
no goals
s : Set Ordinal
a : Ordinal
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
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal := 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
exact enumOrd_mem hs _
case refine'_2
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ o
case refine'_2
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ o
rw [isClosed_iff_bsup] at h
case refine'_2
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), 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
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
case refine'_2
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ o
suffices : enumOrd s a ≤ bsup.{u, u} a fun b (_ : b < a) => enumOrd s b
case this
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
case refine'_2
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), 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
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
exact this.trans (bsup_le H)
case this.intro
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
case this
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
cases' enumOrd_surjective hs _
    (h ha.1 (fun b _ => enumOrd s b) fun b _ => enumOrd_mem hs b) with
  b hb
case this.intro
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ enumOrd s a ≤ enumOrd s b
case this.intro
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ enumOrd s a ≤ bsup a fun b x => enumOrd s b
rw [← hb]
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ a ≤ b
case this.intro
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ enumOrd s a ≤ enumOrd s b
apply Hs.monotone
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
hba : b < a
⊢ False
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
⊢ a ≤ b
by_contra' hba
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
hba : b < a
⊢ enumOrd s (succ b) ≤ enumOrd s b
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
hba : b < a
⊢ False
apply (Hs (lt_succ b)).not_le
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
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
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
hb : enumOrd s b = bsup a fun b x => enumOrd s b
hba : b < a
⊢ enumOrd s (succ b) ≤ enumOrd s b
rw [hb]
no goals
case this.intro.a
s : Set Ordinal
a✝ : Ordinal
hs : Set.Unbounded (fun x x_1 => x < x_1) s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
a : Ordinal
ha : IsLimit a
o : Ordinal
H : ∀ (b : Ordinal), b < a → enumOrd s b ≤ o
b : Ordinal
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
exact le_bsup.{u, u} _ _ (ha.2 _ hba)