α : Type ?u.376990
β : Type ?u.376993
γ : Type ?u.376996
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
f : ι → Ordinal
a : Ordinal
ha : a < mex f
ha' : ∀ (i : ι), f i ≠ a
⊢ False
α : Type ?u.376990
β : Type ?u.376993
γ : Type ?u.376996
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
f : ι → Ordinal
a : Ordinal
ha : a < mex f
⊢ ∃ i, f i = a
by_contra' ha'
no goals
α : Type ?u.376990
β : Type ?u.376993
γ : Type ?u.376996
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
f : ι → Ordinal
a : Ordinal
ha : a < mex f
ha' : ∀ (i : ι), f i ≠ a
⊢ False
exact ha.not_le (mex_le_of_ne ha')