α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ m = n
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
⊢ m = n
letI := Classical.decEq α
case h
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ False
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ m = n
exfalso
case h
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ Classical.choose
      (_ :
        ∃ x,
          ¬x ∈
              Multiset.toFinset
                (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
                  (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n))) ∈
    Multiset.toFinset
      (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
        (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n))
case h
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ False
refine'
  (Classical.choose_spec
      (exists_not_mem_finset
        ((Multiset.range n).pmap (fun m (_hm : m < n) => natEmbeddingAux α m) fun _ =>
            Multiset.mem_range.1).toFinset))
    _
case h
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ Infinite.natEmbeddingAux α m =
    Classical.choose
      (_ :
        ∃ x,
          ¬x ∈
              Multiset.toFinset
                (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
                  (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n)))
case h
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ Classical.choose
      (_ :
        ∃ x,
          ¬x ∈
              Multiset.toFinset
                (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
                  (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n))) ∈
    Multiset.toFinset
      (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
        (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n))
refine' Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, _⟩)
no goals
case h
α✝ : Type ?u.79982
β : Type ?u.79985
γ : Type ?u.79988
α : Type u_1
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ Infinite.natEmbeddingAux α m =
    Classical.choose
      (_ :
        ∃ x,
          ¬x ∈
              Multiset.toFinset
                (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
                  (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n)))
rw [h, natEmbeddingAux]