-- Mathlib/Data/Fintype/EquivFin.lean
theorem natEmbeddingAux_injective (α : Type*) [Infinite α] :
    Function.Injective (natEmbeddingAux α)

Proof state:
α : Type u_4
inst✝ : Infinite α
⊢ Injective (Infinite.natEmbeddingAux α)

Tactic:
rintro m n h

Result:
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
⊢ m = n

Proof state:
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n

Tactic:
wlog hmlen : m ≤ n generalizing m n

Result:
case inr
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this✝ : DecidableEq α := Classical.decEq α
this : ∀ ⦃m n : ℕ⦄, Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n → m ≤ n → m = n
hmlen : ¬m ≤ n
⊢ m = n

α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
⊢ m = n

Proof state:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ Classical.choose ⋯ ∈ (Multiset.pmap (fun m x => Infinite.natEmbeddingAux α m) (Multiset.range n) ⋯).toFinset

Tactic:
refine Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, ?_⟩)

Result:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ Infinite.natEmbeddingAux α m = Classical.choose ⋯

Proof state:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ False

Tactic:
refine (Classical.choose_spec (exists_not_mem_finset
  ((Multiset.range n).pmap (fun m (_ : m < n) ↦ natEmbeddingAux α m)
    (fun _ ↦ Multiset.mem_range.1)).toFinset)) ?_

Result:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ Classical.choose ⋯ ∈ (Multiset.pmap (fun m x => Infinite.natEmbeddingAux α m) (Multiset.range n) ⋯).toFinset

Proof state:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn : ¬m = n
⊢ False

Tactic:
have hmn : m < n := lt_of_le_of_ne hmlen hmn

Result:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ False

Proof state:
case inr
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this✝ : DecidableEq α := Classical.decEq α
this : ∀ ⦃m n : ℕ⦄, Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n → m ≤ n → m = n
hmlen : ¬m ≤ n
⊢ m = n

Tactic:
exact (this h.symm <| le_of_not_le hmlen).symm

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
⊢ m = n

Tactic:
by_contra hmn

Result:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn : ¬m = n
⊢ False

Proof state:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ Infinite.natEmbeddingAux α m = Classical.choose ⋯

Tactic:
rw [h, natEmbeddingAux]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
⊢ m = n

Tactic:
letI := Classical.decEq α

Result:
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n