awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n_1 : ℕ
p : α → Prop
v_1 : Vector3 α n_1
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h_1 : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ ∀ (n_2 : Fin2 n), p ((a :: v) n_2.fs)

Tactic:
h

Premises used: Vector3.cons, Fin2.cases'
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n_1 : ℕ
p : α → Prop
v_1 : Vector3 α n_1
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h_1 : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)

Tactic:
exacts [pa, h]
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
refine_2 :
  ∀ {n : ℕ} (a : α) (v : Vector3 α n) (IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i))
    (h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)), p a
refine_2₁ :
  ∀ {n : ℕ} (a : α) (v : Vector3 α n) (IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i))
    (h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)) (i : Fin2 n), p (v i)
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (p a ∧ VectorAllP p w ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Tactic:
refine fun {n} a v IH =>
      (and_congr_right fun _ => IH).trans
        ⟨fun ⟨pa, h⟩ i => by
          refine i.cases' ?_ ?_
          exacts [pa, h], fun h => ⟨?_, fun i => ?_⟩⟩

Premises used: and_congr_right, And.intro, Iff.intro, Iff.trans
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n_1 : ℕ
p : α → Prop
v_1 : Vector3 α n_1
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
⊢ p a

Tactic:
simpa using h fz

Premises used: Fin2.fz
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n_1 : ℕ
p : α → Prop
v_1 : Vector3 α n_1
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
i : Fin2 n
⊢ p (v i)

Tactic:
simpa using h (fs i)

Premises used: Fin2.fs
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p q : α → Prop
h : ∀ (x : α), p x → q x
v : Vector3 α n
al : VectorAllP p v
⊢ VectorAllP q v

Tactic:
(vectorAllP_iff_forall _ _).2 fun _ => h _ <| (vectorAllP_iff_forall _ _).1 al _

Premises used: Iff.mpr, Iff.mp, vectorAllP_iff_forall
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType β
a₂ : α
f₂ : β a₂ → WType β
h : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₂ f₂)
obtain :
  ∀ (f₂ : β a₁ → WType β) (h : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₁ f₂))
    (h :
      HEq (α := β a₁ → γ) fun (b : β a₁) ↦ elim (β := β) γ fγ (f₁ b) (β := β a₁ → γ) fun (b : β a₁) ↦
        elim (β := β) γ fγ (f₂ b)),
    mk (β := β) a₁ f₁ = mk (β := β) a₁ f₂
⊢ mk (β := β) a₁ f₁ = mk (β := β) a₂ f₂

Tactic:
obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)

Premises used: Iff.mp, Sigma.mk.inj_iff, rfl
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h_1 : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₁ f₂)
h :
  HEq (α := β a₁ → γ) fun (b : β a₁) ↦ elim (β := β) γ fγ (f₁ b) (β := β a₁ → γ) fun (b : β a₁) ↦
    elim (β := β) γ fγ (f₂ b)
e_f : ∀ (x : β a₁), f₁ x = f₂ x
⊢ mk (β := β) a₁ f₁ = mk (β := β) a₁ f₂

Tactic:
congr with x
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h_1 : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₁ f₂)
h :
  HEq (α := β a₁ → γ) fun (b : β a₁) ↦ elim (β := β) γ fγ (f₁ b) (β := β a₁ → γ) fun (b : β a₁) ↦
    elim (β := β) γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x

Tactic:
elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x :)

Premises used: eq_of_heq, congr_fun
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h_1 : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₁ f₂)
h :
  HEq (α := β a₁ → γ) fun (b : β a₁) ↦ elim (β := β) γ fγ (f₁ b) (β := β a₁ → γ) fun (b : β a₁) ↦
    elim (β := β) γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x

Tactic:
exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x :)

Premises used: eq_of_heq, congr_fun
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
hα : IsEmpty α
⊢ IsEmpty (WType β)

Tactic:
⟨fun w => WType.recOn w (IsEmpty.elim hα)⟩

Premises used: WType.recOn, IsEmpty.mk
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
⊢ b ≠ a

Tactic:
have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False

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

Premises used: not_injective_infinite_finite, Nat.recOn
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n :
  Function.Injective (β := WType β) fun (n : ℕ) ↦
    have this : WType β :=
      Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
        mk (β := β) a fun (x : β a) ↦ ih;
    this
⊢ False

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

Premises used: not_injective_infinite_finite, Nat.recOn
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      0)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
zero :
  ∀
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)),
    Eq (α := ℕ) 0 0
zero₁ :
  ∀ (m : ℕ)
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          (m + 1))),
    0 = m + 1
⊢ 0 = m

Tactic:
rcases m with - | m
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      0)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      0)
⊢ Eq (α := ℕ) 0 0

Tactic:
simp_all
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      0)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (m + 1))
⊢ 0 = m + 1

Tactic:
simp_all
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
succ :
  ∀
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          (n + 1))
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)),
    n + 1 = 0
succ₁ :
  ∀ (m : ℕ)
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          (n + 1))
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          (m + 1))),
    n + 1 = m + 1
⊢ n + 1 = m

Tactic:
rcases m with - | m
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      0)
⊢ n + 1 = 0

Tactic:
simp_all
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (m + 1))
⊢ n + 1 = m + 1

Tactic:
congr_arg Nat.succ (ih ?_)

Premises used: congr_arg, Nat.succ
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (m + 1))
succ :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      n)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
⊢ n + 1 = m + 1

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

Premises used: congr_arg, Nat.succ
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          n)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n = m
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (n + 1))
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      (m + 1))
⊢ Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      n)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)

Tactic:
simp_all [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      n)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
zero :
  ∀ ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          0)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    0 = m
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ ⦃m : ℕ⦄
        (h :
          Eq (α := WType β)
            ((fun (n : ℕ) ↦
                have this : WType β :=
                  Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                    mk (β := β) a fun (x : β a) ↦ ih;
                this)
              n)
            ((fun (n : ℕ) ↦
                have this : WType β :=
                  Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                    mk (β := β) a fun (x : β a) ↦ ih;
                this)
              m)),
        n = m)
    ⦃m : ℕ⦄
    (h :
      Eq (α := WType β)
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          (n + 1))
        ((fun (n : ℕ) ↦
            have this : WType β :=
              Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
                mk (β := β) a fun (x : β a) ↦ ih;
            this)
          m)),
    n + 1 = m
⊢ n = m

Tactic:
induction n generalizing m with
    | zero => rcases m with - | m <;> simp_all
    | succ n ih =>
      rcases m with - | m
      · simp_all
      · refine congr_arg Nat.succ (ih ?_)
        simp_all [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
t : WType β
mk : ∀ (a : α) (f : β a → WType β), 0 < (WType.mk (β := β) a f).depth (β := β)
⊢ 0 < t.depth (β := β)

Tactic:
cases t
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
a : α
f : β a → WType β
⊢ 0 < (mk (β := β) a f).depth (β := β)

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
a : α
f : β a → WType β
i : β a
⊢ (f i).depth (β := β) < (mk (β := β) a f).depth (β := β)

Tactic:
Nat.lt_succ_of_le (Finset.le_sup (f := (depth <| f ·)) (Finset.mem_univ i))

Premises used: Finset.mem_univ, Nat.lt_succ_of_le, WType.depth, Finset.le_sup
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
f : WType' β 0 → Empty :=
  fun (x : WType' β 0) ↦
    match (motive := WType' β 0 → Empty) x with
    | ⟨val, h⟩ => ⋯.elim
x : Empty
⊢ WType' β 0

Tactic:
cases x
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
n : ℕ
t : WType β
h : t.depth (β := β) ≤ n + 1
obtain : (a : α) → (f : β a → WType β) → (h : (mk (β := β) a f).depth (β := β) ≤ n + 1) → (a : α) × (β a → WType' β n)
⊢ (a : α) × (β a → WType' β n)

Tactic:
obtain ⟨a, f⟩ := t
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
n : ℕ
a : α
f : β a → WType β
h : (mk (β := β) a f).depth (β := β) ≤ n + 1
⊢ ∀ (i : β a), (f i).depth (β := β) ≤ n

Tactic:
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)
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
n : ℕ
a : α
f : β a → WType β
h : (mk (β := β) a f).depth (β := β) ≤ n + 1
h₀ : ∀ (i : β a), (f i).depth (β := β) ≤ n
⊢ (a : α) × (β a → WType' β n)

Tactic:
exact ⟨a, fun i : β a => ⟨f i, h₀ i⟩⟩
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
inst_2 : Encodable α
n : ℕ
x : Encodable (WType' β n)
a : α
f : β a → WType β
property : (mk (β := β) a f).depth (β := β) ≤ n + 1
⊢ Eq (α := WType' β (n + 1))
    (finv (β := β) n
      (WType.f (β := β) n (Subtype.mk (p := fun (t : WType β) ↦ t.depth (β := β) ≤ n + 1) (mk (β := β) a f) property)))
    (Subtype.mk (p := fun (t : WType β) ↦ t.depth (β := β) ≤ n + 1) (mk (β := β) a f) property)

Tactic:
rfl
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
inst_2 : Encodable α
haveI : (h' : (n : ℕ) → Encodable (WType' β n)) → Encodable (WType β)
⊢ Encodable (WType β)

Tactic:
haveI h' : ∀ n, Encodable (WType' β n) := fun n => Nat.rec encodable_zero encodable_succ n
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
inst_2 : Encodable α
h' : (n : ℕ) → Encodable (WType' β n)
f : WType β → (n : ℕ) × WType' β n :=
  fun (t : WType β) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ WType' β n) (t.depth (β := β))
      (Subtype.mk (p := fun (t_1 : WType β) ↦ t_1.depth (β := β) ≤ t.depth (β := β)) t ⋯)
finv : (n : ℕ) × WType' β n → WType β :=
  fun (p : (n : ℕ) × WType' β n) ↦ (↑(p.snd (β := fun (n : ℕ) ↦ WType' β n)) : WType β)
⊢ ∀ (t : WType β), finv (f t) = t

Tactic:
have : ∀ t, finv (f t) = t := fun t => rfl