α : Type ?u.365393
β : Type ?u.365396
γ : Type ?u.365399
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.365393
β : Type ?u.365396
γ : Type ?u.365399
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.365393
β : Type ?u.365396
γ : Type ?u.365399
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