-- Mathlib/Data/W/Basic.lean
theorem infinite_of_nonempty_of_isEmpty (a b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)] :
    Infinite (WType β) :=
  ⟨by
    intro hf
    have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
    refine
      not_injective_infinite_finite
        (fun n : ℕ =>
          show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩)
        ?_
    intro n m h
    induction' n with n ih generalizing m
    · rcases m with - | m <;> simp_all
    · rcases m with - | m
      · simp_all
      · refine congr_arg Nat.succ (ih ?_)
        simp_all [funext_iff]⟩

Proof state:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False

Tactic:
refine
  not_injective_infinite_finite
    (fun n : ℕ =>
      show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩)
    ?_

Result:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ Function.Injective fun n =>
    let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
    this

Proof state:
case succ.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      0
⊢ n + 1 = 0

Tactic:
simp_all

Result:
no goals

Proof state:
case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (m + 1)
⊢ (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m

Tactic:
simp_all [funext_iff]

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ Function.Injective fun n =>
    let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
    this

Tactic:
intro n m h

Result:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m
⊢ n = m

Proof state:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
⊢ False

Tactic:
have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))

Result:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False

Proof state:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
⊢ ¬Finite (WType β)

Tactic:
intro hf

Result:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
⊢ False

Proof state:
case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (m + 1)
⊢ n + 1 = m + 1

Tactic:
refine congr_arg Nat.succ (ih ?_)

Result:
case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (m + 1)
⊢ (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m

Proof state:
case zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      0 =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m
⊢ 0 = m

Tactic:
rcases m with - | m <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m
⊢ n = m

Tactic:
induction' n with n ih generalizing m

Result:
case zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      0 =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m
⊢ 0 = m

case succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m
⊢ n + 1 = m