α : Type u_2
β : α → Type u_1
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
⊢ False
α : Type u_2
β : α → Type u_1
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
⊢ ¬Finite (WType β)
intro hf
α : Type u_2
β : α → Type u_1
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False
α : Type u_2
β : α → Type u_1
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
⊢ False
have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
    this
α : Type u_2
β : α → Type u_1
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False
refine'
  not_injective_infinite_finite
    (fun n : ℕ =>
      show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩)
    _
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ n = m
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
    this
intro n m h
case zero
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ Nat.zero = m

case succ
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ Nat.succ n = m
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ n = m
induction' n with n ih generalizing m
no goals
case zero
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ Nat.zero = m
cases' m with m <;> simp_all
case succ.zero
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero
⊢ Nat.succ n = Nat.zero

case succ.succ
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ m)
⊢ Nat.succ n = Nat.succ m
case succ
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ Nat.succ n = m
cases' m with m
no goals
case succ.zero
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero
⊢ Nat.succ n = Nat.zero
simp_all
case succ.succ
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ m)
⊢ (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
case succ.succ
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ m)
⊢ Nat.succ n = Nat.succ m
refine' congr_arg Nat.succ (ih _)
no goals
case succ.succ
α : Type u_2
β : α → Type u_1
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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ m)
⊢ (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
simp_all [Function.funext_iff]