α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
⊢ m = n
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
⊢ Injective (Infinite.natEmbeddingAux α)
rintro m n h
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
⊢ m = n
letI := Classical.decEq α
case inl
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
hmn : m < n
⊢ m = n

case inr.inl
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m : ℕ
this : DecidableEq α := Classical.decEq α
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α m
⊢ m = m

case inr.inr
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
hnm : n < m
⊢ m = n
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n
rcases lt_trichotomy m n with hmn | rfl | hnm
no goals
case inl
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
hmn : m < n
⊢ m = n
apply natEmbeddingAux_injective_aux α m n h hmn
no goals
case inr.inl
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m : ℕ
this : DecidableEq α := Classical.decEq α
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α m
⊢ m = m
rfl
no goals
case inr.inr
α✝ : Type ?u.80507
β : Type ?u.80510
γ : Type ?u.80513
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
hnm : n < m
⊢ m = n
apply (natEmbeddingAux_injective_aux α n m h.symm hnm).symm