[GOAL]
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType fun a => β a
a₂ : α
f₂ : β a₂ → WType fun a => β a
h : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₂ f₂)
⊢ mk a₁ f₁ = mk a₂ f₂
[PROOFSTEP]
obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)
[GOAL]
case intro
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
⊢ mk a₁ f₁ = mk a₁ f₂
[PROOFSTEP]
congr with x
[GOAL]
case intro.e_f.h
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x
[PROOFSTEP]
exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x : _)
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
⊢ ¬Finite (WType β)
[PROOFSTEP]
intro hf
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
⊢ False
[PROOFSTEP]
have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False
[PROOFSTEP]
refine'
  not_injective_infinite_finite
    (fun n : ℕ => show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩) _
[GOAL]
α : 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 (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
    this
[PROOFSTEP]
intro n m h
[GOAL]
α : 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 (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
[PROOFSTEP]
induction' n with n ih generalizing m
[GOAL]
case zero
α : 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 (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
[PROOFSTEP]
cases' m with m
[GOAL]
case zero.zero
α : 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 (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
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)
      Nat.zero
⊢ Nat.zero = Nat.zero
[PROOFSTEP]
simp_all
[GOAL]
case zero.succ
α : 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 (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)
      (Nat.succ m)
⊢ Nat.zero = Nat.succ m
[PROOFSTEP]
simp_all
[GOAL]
case succ
α : 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 (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
[PROOFSTEP]
cases' m with m
[GOAL]
case succ.zero
α : 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 (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
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
α : 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 (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
[PROOFSTEP]
refine' congr_arg Nat.succ (ih _)
[GOAL]
case succ.succ
α : 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 (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
[PROOFSTEP]
simp_all [Function.funext_iff]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < depth t
[PROOFSTEP]
cases t
[GOAL]
case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < depth (mk a✝ f✝)
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
f : WType.WType' β 0 → Empty :=
  fun x =>
    match x with
    | { val := x, property := h } => False.elim (_ : False)
⊢ Empty → WType.WType' β 0
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
f : WType.WType' β 0 → Empty :=
  fun x =>
    match x with
    | { val := x, property := h } => False.elim (_ : False)
x : Empty
⊢ WType.WType' β 0
[PROOFSTEP]
cases x
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
t : WType β
h : depth t ≤ n + 1
⊢ (a : α) × (β a → WType.WType' β n)
[PROOFSTEP]
cases' t with a f
[GOAL]
case mk
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
a : α
f : β a → WType β
h : depth (mk a f) ≤ n + 1
⊢ (a : α) × (β a → WType.WType' β n)
[PROOFSTEP]
have h₀ : ∀ i : β a, WType.depth (f i) ≤ n := fun i =>
  Nat.le_of_lt_succ (lt_of_lt_of_le (WType.depth_lt_depth_mk a f i) h)
[GOAL]
case mk
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
a : α
f : β a → WType β
h : depth (mk a f) ≤ n + 1
h₀ : ∀ (i : β a), depth (f i) ≤ n
⊢ (a : α) × (β a → WType.WType' β n)
[PROOFSTEP]
exact ⟨a, fun i : β a => ⟨f i, h₀ i⟩⟩
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
n : ℕ
h : Encodable (WType.WType' β n)
⊢ ∀ (b : WType.WType' β (n + 1)), WType.finv n (WType.f n b) = b
[PROOFSTEP]
rintro ⟨⟨_, _⟩, _⟩
[GOAL]
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
n : ℕ
h : Encodable (WType.WType' β n)
a✝ : α
f✝ : β a✝ → WType β
property✝ : depth (mk a✝ f✝) ≤ n + 1
⊢ WType.finv n (WType.f n { val := mk a✝ f✝, property := property✝ }) = { val := mk a✝ f✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
⊢ Encodable (WType β)
[PROOFSTEP]
haveI h' : ∀ n, Encodable (WType' β n) := fun n => Nat.rec encodable_zero encodable_succ n
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
⊢ Encodable (WType β)
[PROOFSTEP]
let f : WType β → Σ n, WType' β n := fun t => ⟨t.depth, ⟨t, le_rfl⟩⟩
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
f : WType β → (n : ℕ) × WType.WType' β n :=
  fun t => { fst := depth t, snd := { val := t, property := (_ : depth t ≤ depth t) } }
⊢ Encodable (WType β)
[PROOFSTEP]
let finv : (Σ n, WType' β n) → WType β := fun p => p.2.1
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
f : WType β → (n : ℕ) × WType.WType' β n :=
  fun t => { fst := depth t, snd := { val := t, property := (_ : depth t ≤ depth t) } }
finv : (n : ℕ) × WType.WType' β n → WType β := fun p => ↑p.snd
⊢ Encodable (WType β)
[PROOFSTEP]
have : ∀ t, finv (f t) = t := fun t => rfl
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
f : WType β → (n : ℕ) × WType.WType' β n :=
  fun t => { fst := depth t, snd := { val := t, property := (_ : depth t ≤ depth t) } }
finv : (n : ℕ) × WType.WType' β n → WType β := fun p => ↑p.snd
this : ∀ (t : WType β), finv (f t) = t
⊢ Encodable (WType β)
[PROOFSTEP]
exact Encodable.ofLeftInverse f finv this
