awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
refine :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β v v' fs
⊢ β v v' fs

Tactic:
refine cast ?_ f

Premises used: cast
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
h : ∀ (i : Fin2 0), v i = i.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
⊢ v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
i : Fin2 0
⊢ v i = i.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)

Tactic:
contradiction
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
⊢ v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)

Tactic:
have eq₁ : v = Fin2.elim0 := by funext i; contradiction
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
h : ∀ (i : Fin2 0), v' i = i.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
⊢ v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
i : Fin2 0
⊢ v' i = i.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)

Tactic:
contradiction
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
⊢ v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)

Tactic:
have eq₂ : v' = Fin2.elim0 := by funext i; contradiction
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
h : ∀ (i : Fin2 0), fs i = nilFun (α := v) (β := v') i
⊢ fs = nilFun (α := v) (β := v')

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
i : Fin2 0
⊢ fs i = nilFun (α := v) (β := v') i

Tactic:
contradiction
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
⊢ fs = nilFun (α := v) (β := v')

Tactic:
have eq₃ : fs = nilFun := by funext i; contradiction
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
eq₃ : fs = nilFun (α := v) (β := v')
refl :
  ∀ (fs : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v')
    (eq₃ : fs = nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := v')),
    β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
        (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
          Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
      β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v' fs
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β v v' fs

Tactic:
cases eq₁
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v' : TypeVec.{u_3} 0
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
fs : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v'
eq₃ : fs = nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := v')
refl :
  ∀
    (fs :
      Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)))
    (eq₃ :
      fs =
        nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β :=
          Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3))),
    β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
        (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
          Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
      β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)) fs
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v' fs

Tactic:
cases eq₂
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
fs : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3))
eq₃ :
  fs = nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3))
refl :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)))
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)) fs

Tactic:
cases eq₃
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)))

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
β : (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type u_2) →
    (t' : Type u_3) →
      (f : t → t') →
        (v : TypeVec.{u_2} n) →
          (v' : TypeVec.{u_3} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (appendFun (α := v) (α' := v') fs f)
v : TypeVec.{u_2} (n + 1)
v' : TypeVec.{u_3} (n + 1)
rw : (fs : Arrow.{u_2, u_3} (v.drop ::: v.last) (v'.drop ::: v'.last)) → β (v.drop ::: v.last) (v'.drop ::: v'.last) fs
⊢ (fs : v ⟹ v') → β v v' fs

Tactic:
rw [← append1_drop_last v, ← append1_drop_last v']

Premises used: TypeVec.append1_drop_last
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
β : (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type u_2) →
    (t' : Type u_3) →
      (f : t → t') →
        (v : TypeVec.{u_2} n) →
          (v' : TypeVec.{u_3} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (appendFun (α := v) (α' := v') fs f)
v : TypeVec.{u_2} (n + 1)
v' : TypeVec.{u_3} (n + 1)
fs : Arrow.{u_2, u_3} (v.drop ::: v.last) (v'.drop ::: v'.last)
rw :
  β (v.drop ::: v.last) (v'.drop ::: v'.last)
    (splitFun (α := v.drop ::: v.last) (α' := v'.drop ::: v'.last)
      (dropFun (α := v.drop ::: v.last) (β := v'.drop ::: v'.last) fs)
      (lastFun (α := v.drop ::: v.last) (β := v'.drop ::: v'.last) fs))
⊢ β (v.drop ::: v.last) (v'.drop ::: v'.last) fs

Tactic:
rw [← split_dropFun_lastFun fs]

Premises used: TypeVec.split_dropFun_lastFun
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
β : (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type u_2) →
    (t' : Type u_3) →
      (f : t → t') →
        (v : TypeVec.{u_2} n) →
          (v' : TypeVec.{u_3} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (appendFun (α := v) (α' := v') fs f)
v : TypeVec.{u_2} (n + 1)
v' : TypeVec.{u_3} (n + 1)
fs : Arrow.{u_2, u_3} (v.drop ::: v.last) (v'.drop ::: v'.last)
⊢ β (v.drop ::: v.last) (v'.drop ::: v'.last)
    (splitFun (α := v.drop ::: v.last) (α' := v'.drop ::: v'.last)
      (dropFun (α := v.drop ::: v.last) (β := v'.drop ::: v'.last) fs)
      (lastFun (α := v.drop ::: v.last) (β := v'.drop ::: v'.last) fs))

Tactic:
apply F
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β :
  Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)) →
    Sort u_1
f : β (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
g : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
this :
  g = nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
rwa rwa₁ rwa₂ rwa₃ :
  β (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
⊢ β g

Tactic:
rwa [this]
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β :
  Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)) →
    Sort u_1
f : β (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
g : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
suffices :
  g = nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
⊢ β g

Tactic:
suffices g = nilFun by rwa [this]
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β :
  Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)) →
    Sort u_1
f : β (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
g : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
⊢ g = nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))

Tactic:
ext ⟨⟩
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : Arrow.{u_1, u_2} (v ::: t) (v' ::: t') → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (appendFun (α := v) (α' := v') fs f)
fs : Arrow.{u_1, u_2} (v ::: t) (v' ::: t')
rw :
  β
    (splitFun (α := v ::: t) (α' := v' ::: t') (dropFun (α := v ::: t) (β := v' ::: t') fs)
      (lastFun (α := v ::: t) (β := v' ::: t') fs))
⊢ β fs

Tactic:
rw [← split_dropFun_lastFun fs]

Premises used: TypeVec.split_dropFun_lastFun
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : Arrow.{u_1, u_2} (v ::: t) (v' ::: t') → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (appendFun (α := v) (α' := v') fs f)
fs : Arrow.{u_1, u_2} (v ::: t) (v' ::: t')
⊢ β
    (splitFun (α := v ::: t) (α' := v' ::: t') (dropFun (α := v ::: t) (β := v' ::: t') fs)
      (lastFun (α := v ::: t) (β := v' ::: t') fs))

Tactic:
apply F
-- Module: Mathlib.Data.TypeVec
Goal:
β :
  Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)) →
    Sort u_1
f : β (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
⊢ typevecCasesNil₂ (β := β) f
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    f

Tactic:
rfl

Premises used: Eq.mpr, TypeVec.typevecCasesNil₂, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : Arrow.{u_1, u_2} (v ::: t) (v' ::: t') → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (appendFun (α := v) (α' := v') fs f)
f : t → t'
fs : v ⟹ v'
⊢ typevecCasesCons₂ n t t' v v' (β := β) F (appendFun (α := v) (α' := v') fs f) = F f fs

Tactic:
rfl

Premises used: Eq.mpr, TypeVec.typevecCasesCons₂, TypeVec.lastFun, TypeVec.appendFun, TypeVec.splitFun, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
a :
  ∀ (i : Fin2 (n + 1)),
    TypeVec.const x (α ::: β) i = appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) i
⊢ TypeVec.const x (α ::: β) = appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) fun (x_1 : β) ↦ x

Tactic:
ext i : 1
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
a :
  Eq (α := (α ::: β) Fin2.fz → «repeat» (n + 1) γ Fin2.fz) (TypeVec.const x (α ::: β) Fin2.fz)
    (appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) Fin2.fz)
a₁ :
  ∀ (a : Fin2 n),
    Eq (α := (α ::: β) a.fs → «repeat» (n + 1) γ a.fs) (TypeVec.const x (α ::: β) a.fs)
      (appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) a.fs)
⊢ TypeVec.const x (α ::: β) i = appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) i

Tactic:
cases i
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ Eq (α := (α ::: β) Fin2.fz → «repeat» (n + 1) γ Fin2.fz) (TypeVec.const x (α ::: β) Fin2.fz)
    (appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) Fin2.fz)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
a : Fin2 n
⊢ Eq (α := (α ::: β) a.fs → «repeat» (n + 1) γ a.fs) (TypeVec.const x (α ::: β) a.fs)
    (appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) a.fs)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
a : ∀ (x : Fin2 0) (x_1 : α x), f x x_1 = nilFun (α := α) (β := β) x x_1
⊢ f = nilFun (α := α) (β := β)

Tactic:
ext x
-- Module: Mathlib.Data.TypeVec
Goal:
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
x : Fin2 0
x_1 : α x
⊢ f x x_1 = nilFun (α := α) (β := β) x x_1

Tactic:
cases x
-- Module: Mathlib.Data.TypeVec
Goal:
α : TypeVec.{u_1} 0
a : ∀ (x : Fin2 0) (x_1 : α x), id (α := α) x x_1 = nilFun (α := α) (β := α) x x_1
⊢ Eq.{u_1 + 1} (α := α ⟹ α) (id (α := α)) (nilFun (α := α) (β := α))

Tactic:
ext x
-- Module: Mathlib.Data.TypeVec
Goal:
α : TypeVec.{u_1} 0
x : Fin2 0
x_1 : α x
⊢ id (α := α) x x_1 = nilFun (α := α) (β := α) x x_1

Tactic:
cases x
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
x : β
α : TypeVec.{u_2} 0
a : ∀ (i : Fin2 0), TypeVec.const x α i = nilFun (α := α) (β := «repeat» 0 β) i
⊢ TypeVec.const x α = nilFun (α := α) (β := «repeat» 0 β)

Tactic:
ext i : 1
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
x : β
α : TypeVec.{u_2} 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun (α := α) (β := «repeat» 0 β) i

Tactic:
cases i
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
n : ℕ
α : TypeVec.{u_1} n
zero :
  ∀ (α : TypeVec.{u_1} 0),
    (α ::: β).repeatEq =
      splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» 0 Prop ::: Prop) α.repeatEq
        (uncurry Eq)
succ :
  ∀ (n : ℕ),
    (∀ (α : TypeVec.{u_1} n),
        (α ::: β).repeatEq =
          splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» n Prop ::: Prop) α.repeatEq
            (uncurry Eq)) →
      ∀ (α : TypeVec.{u_1} (n + 1)),
        (α ::: β).repeatEq =
          splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» (n + 1) Prop ::: Prop)
            α.repeatEq (uncurry Eq)
⊢ (α ::: β).repeatEq =
    splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» n Prop ::: Prop) α.repeatEq
      (uncurry Eq)

Tactic:
induction n
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
α : TypeVec.{u_1} 0
⊢ (α ::: β).repeatEq =
    splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» 0 Prop ::: Prop) α.repeatEq
      (uncurry Eq)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
β : Type u_1
n : ℕ
h :
  ∀ (α : TypeVec.{u_1} n),
    (α ::: β).repeatEq =
      splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» n Prop ::: Prop) α.repeatEq
        (uncurry Eq)
α : TypeVec.{u_1} (n + 1)
⊢ (α ::: β).repeatEq =
    splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» (n + 1) Prop ::: Prop) α.repeatEq
      (uncurry Eq)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
α : TypeVec.{u_1} 0
a : ∀ (i : Fin2 0) (x : (α ⊗ α) i), α.repeatEq i x = nilFun (α := α ⊗ α) (β := «repeat» 0 Prop) i x
⊢ α.repeatEq = nilFun (α := α ⊗ α) (β := «repeat» 0 Prop)

Tactic:
ext i
-- Module: Mathlib.Data.TypeVec
Goal:
α : TypeVec.{u_1} 0
i : Fin2 0
x : (α ⊗ α) i
⊢ α.repeatEq i x = nilFun (α := α ⊗ α) (β := «repeat» 0 Prop) i x

Tactic:
cases i
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
p : Prop
n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
p : Prop
n_1 : ℕ
a : Fin2 n_1
ih : ∀ {α : TypeVec.{u_1} n_1} {x : α a}, ofRepeat (TypeVec.const p α a x) ↔ p
α : TypeVec.{u_1} (n_1 + 1)
x : α a.fs
fs : ofRepeat (TypeVec.const.{0, u_1} p α.drop a x) ↔ p
⊢ ofRepeat (TypeVec.const p α a.fs x) ↔ p

Tactic:
rw [TypeVec.const]

Premises used: TypeVec.const
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
p : Prop
n_1 : ℕ
a : Fin2 n_1
ih : ∀ {α : TypeVec.{u_1} n_1} {x : α a}, ofRepeat (TypeVec.const p α a x) ↔ p
α : TypeVec.{u_1} (n_1 + 1)
x : α a.fs
⊢ ofRepeat (TypeVec.const.{0, u_1} p α.drop a x) ↔ p

Tactic:
ih

Premises used: TypeVec.ofRepeat
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
p : Prop
n_1 : ℕ
a : Fin2 n_1
ih : ∀ {α : TypeVec.{u_1} n_1} {x : α a}, ofRepeat (TypeVec.const p α a x) ↔ p
α : TypeVec.{u_1} (n_1 + 1)
x : α a.fs
⊢ ofRepeat (TypeVec.const.{0, u_1} p α.drop a x) ↔ p

Tactic:
exact ih
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
p : Prop
fz : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {x : α Fin2.fz}, ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p
fs :
  ∀ {n : ℕ} (a : Fin2 n) (ih : ∀ {α : TypeVec.{u_1} n} {x : α a}, ofRepeat (TypeVec.const p α a x) ↔ p)
    {α : TypeVec.{u_1} (n + 1)} {x : α a.fs}, ofRepeat (TypeVec.const p α a.fs x) ↔ p
⊢ ofRepeat (TypeVec.const p α i x) ↔ p

Tactic:
induction i with
  | fz => rfl
  | fs _ ih =>
    rw [TypeVec.const]
    exact ih

Premises used: TypeVec.const
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α β : TypeVec.{u_1} (n_1 + 1)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.fst (α := α) (β := β) Fin2.fz (prod.mk (α := α) (β := β) Fin2.fz a b) = a

Tactic:
simp_all only [prod.fst, prod.mk]

Premises used: TypeVec.prod.mk, TypeVec.prod.fst
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a_1 : Fin2 n_1
i_ih :
  ∀ {α β : TypeVec.{u_1} n_1} (a : α a_1) (b : β a_1),
    prod.fst (α := α) (β := β) a_1 (prod.mk (α := α) (β := β) a_1 a b) = a
α β : TypeVec.{u_1} (n_1 + 1)
a : α a_1.fs
b : β a_1.fs
⊢ prod.fst (α := α) (β := β) a_1.fs (prod.mk (α := α) (β := β) a_1.fs a b) = a

Tactic:
apply i_ih