α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
a : Ordinal
ha : a < o'
⊢ g a ha < blsub o' g
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
a : Ordinal
ha : a < o'
⊢ g a ha < o
rw [← hg]
no goals
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
a : Ordinal
ha : a < o'
⊢ g a ha < blsub o' g
apply lt_blsub
case a
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi : i < o'
⊢ f (g i hi) (_ : g i hi < o) ≤ bsup o f

case a
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi : i < o
⊢ f i hi ≤ bsup o' fun a ha => f (g a ha) (_ : g a ha < o)
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
⊢ (bsup o' fun a ha => f (g a ha) (_ : g a ha < o)) = bsup o f
apply le_antisymm <;> refine' bsup_le fun i hi => _
no goals
case a
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi : i < o'
⊢ f (g i hi) (_ : g i hi < o) ≤ bsup o f
apply le_bsup
case a
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi✝ : i < o
hi : ∃ i_1 hi, i ≤ g i_1 hi
⊢ f i hi✝ ≤ bsup o' fun a ha => f (g a ha) (_ : g a ha < o)
case a
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi : i < o
⊢ f i hi ≤ bsup o' fun a ha => f (g a ha) (_ : g a ha < o)
rw [← hg, lt_blsub_iff] at hi
case a.intro.intro
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi : i < o
j : Ordinal
hj : j < o'
hj' : i ≤ g j hj
⊢ f i hi ≤ bsup o' fun a ha => f (g a ha) (_ : g a ha < o)
case a
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi✝ : i < o
hi : ∃ i_1 hi, i ≤ g i_1 hi
⊢ f i hi✝ ≤ bsup o' fun a ha => f (g a ha) (_ : g a ha < o)
rcases hi with ⟨j, hj, hj'⟩
no goals
case a.intro.intro
α : Type ?u.362805
β : Type ?u.362808
γ : Type ?u.362811
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal) → a < o' → Ordinal
hg : blsub o' g = o
i : Ordinal
hi : i < o
j : Ordinal
hj : j < o'
hj' : i ≤ g j hj
⊢ f i hi ≤ bsup o' fun a ha => f (g a ha) (_ : g a ha < o)
exact (hf _ _ hj').trans (le_bsup _ _ _)