case intro
α : Type ?u.387773
β : Type ?u.387776
γ : Type ?u.387779
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
ha : a < bmex o f
i : (Quotient.out o).α
hi : familyOfBFamily o f i = a
⊢ ∃ i hi, f i hi = a
α : Type ?u.387773
β : Type ?u.387776
γ : Type ?u.387779
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
ha : a < bmex o f
⊢ ∃ i hi, f i hi = a
cases' exists_of_lt_mex ha with i hi
no goals
case intro
α : Type ?u.387773
β : Type ?u.387776
γ : Type ?u.387779
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
ha : a < bmex o f
i : (Quotient.out o).α
hi : familyOfBFamily o f i = a
⊢ ∃ i hi, f i hi = a
exact ⟨_, typein_lt_self i, hi⟩