case intro.intro
α : Type ?u.316558
β : Type ?u.316561
γ : Type ?u.316564
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
i : Ordinal
hi : i < o
j : Ordinal
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ bsup o' g
α : Type ?u.316558
β : Type ?u.316561
γ : Type ?u.316564
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
i : Ordinal
hi : i < o
⊢ f i hi ≤ bsup o' g
obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, rfl⟩
case intro.intro
α : Type ?u.316558
β : Type ?u.316561
γ : Type ?u.316564
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
i : Ordinal
hi : i < o
j : Ordinal
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ bsup o' g
case intro.intro
α : Type ?u.316558
β : Type ?u.316561
γ : Type ?u.316564
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
i : Ordinal
hi : i < o
j : Ordinal
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ bsup o' g
rw [← hj']
no goals
case intro.intro
α : Type ?u.316558
β : Type ?u.316561
γ : Type ?u.316564
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
i : Ordinal
hi : i < o
j : Ordinal
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ bsup o' g
apply le_bsup