α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
⊢ False
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ mex f < ord (succ (#ι))
by_contra' h
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
⊢ succ (#ι) ≤ (#ι)
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
⊢ False
apply (lt_succ (#ι)).not_le
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
⊢ succ (#ι) ≤ (#ι)
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
⊢ succ (#ι) ≤ (#ι)
have H := fun a => exists_of_lt_mex ((typein_lt_self a).trans_le h)
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
g : (Quotient.out (ord (succ (#ι)))).α → ι := fun a => choose (_ : ∃ i, f i = typein (fun x x_1 => x < x_1) a)
⊢ succ (#ι) ≤ (#ι)
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
⊢ succ (#ι) ≤ (#ι)
let g : (succ (#ι)).ord.out.α → ι := fun a => Classical.choose (H a)
case h.e'_3
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
g : (Quotient.out (ord (succ (#ι)))).α → ι := fun a => choose (_ : ∃ i, f i = typein (fun x x_1 => x < x_1) a)
hg : Injective g
⊢ succ (#ι) = (#(Quotient.out (ord (succ (#ι)))).α)
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
g : (Quotient.out (ord (succ (#ι)))).α → ι := fun a => choose (_ : ∃ i, f i = typein (fun x x_1 => x < x_1) a)
hg : Injective g
⊢ succ (#ι) ≤ (#ι)
convert Cardinal.mk_le_of_injective hg
no goals
case h.e'_3
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
g : (Quotient.out (ord (succ (#ι)))).α → ι := fun a => choose (_ : ∃ i, f i = typein (fun x x_1 => x < x_1) a)
hg : Injective g
⊢ succ (#ι) = (#(Quotient.out (ord (succ (#ι)))).α)
rw [Cardinal.mk_ord_out (succ (#ι))]
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
g : (Quotient.out (ord (succ (#ι)))).α → ι := fun a => choose (_ : ∃ i, f i = typein (fun x x_1 => x < x_1) a)
a b : (Quotient.out (ord (succ (#ι)))).α
Hf : ∀ (x : (Quotient.out (ord (succ (#ι)))).α), f (g x) = typein (fun x x_1 => x < x_1) x
h' : f (g a) = f (g b)
⊢ a = b
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
g : (Quotient.out (ord (succ (#ι)))).α → ι := fun a => choose (_ : ∃ i, f i = typein (fun x x_1 => x < x_1) a)
a b : (Quotient.out (ord (succ (#ι)))).α
h' : g a = g b
Hf : ∀ (x : (Quotient.out (ord (succ (#ι)))).α), f (g x) = typein (fun x x_1 => x < x_1) x
⊢ a = b
apply_fun f  at h'
no goals
α : Type ?u.378408
β : Type ?u.378411
γ : Type ?u.378414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : ord (succ (#ι)) ≤ mex f
H : ∀ (a : (Quotient.out (ord (succ (#ι)))).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a
g : (Quotient.out (ord (succ (#ι)))).α → ι := fun a => choose (_ : ∃ i, f i = typein (fun x x_1 => x < x_1) a)
a b : (Quotient.out (ord (succ (#ι)))).α
Hf : ∀ (x : (Quotient.out (ord (succ (#ι)))).α), f (g x) = typein (fun x x_1 => x < x_1) x
h' : f (g a) = f (g b)
⊢ a = b
rwa [Hf, Hf, typein_inj] at h'