α✝ : Type ?u.377983
β✝ : Type ?u.377986
γ : Type ?u.377989
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
f : α → Ordinal
g : β → Ordinal
h : range f ⊆ range g
i : α
hi : f i = mex g
⊢ False
α✝ : Type ?u.377983
β✝ : Type ?u.377986
γ : Type ?u.377989
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
f : α → Ordinal
g : β → Ordinal
h : range f ⊆ range g
⊢ mex f ≤ mex g
refine' mex_le_of_ne fun i hi => _
case intro
α✝ : Type ?u.377983
β✝ : Type ?u.377986
γ : Type ?u.377989
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
f : α → Ordinal
g : β → Ordinal
h : range f ⊆ range g
i : α
hi : f i = mex g
j : β
hj : g j = f i
⊢ False
α✝ : Type ?u.377983
β✝ : Type ?u.377986
γ : Type ?u.377989
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
f : α → Ordinal
g : β → Ordinal
h : range f ⊆ range g
i : α
hi : f i = mex g
⊢ False
cases' h ⟨i, rfl⟩ with j hj
case intro
α✝ : Type ?u.377983
β✝ : Type ?u.377986
γ : Type ?u.377989
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
f : α → Ordinal
g : β → Ordinal
h : range f ⊆ range g
i : α
j : β
hi : g j = mex g
hj : g j = f i
⊢ False
case intro
α✝ : Type ?u.377983
β✝ : Type ?u.377986
γ : Type ?u.377989
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
f : α → Ordinal
g : β → Ordinal
h : range f ⊆ range g
i : α
hi : f i = mex g
j : β
hj : g j = f i
⊢ False
rw [← hj] at hi
no goals
case intro
α✝ : Type ?u.377983
β✝ : Type ?u.377986
γ : Type ?u.377989
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
f : α → Ordinal
g : β → Ordinal
h : range f ⊆ range g
i : α
j : β
hi : g j = mex g
hj : g j = f i
⊢ False
exact ne_mex g j hi