awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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))
⊢ β (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
have 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)))
Tactic: cases eq₃
Cleared hypotheses: fs, eq₃
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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 : v ⟹ v') → β v v' fs
have rw : (fs : Arrow.{u_2, u_3} (v.drop ::: v.last) (v'.drop ::: v'.last)) → β (v.drop ::: v.last) (v'.drop ::: v'.last) fs
Tactic: rw [← append1_drop_last v, ← append1_drop_last v']
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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) fs
have 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))
Tactic: rw [← split_dropFun_lastFun fs]
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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
have suffices : g = nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
Tactic: suffices g = nilFun by rwa [this]
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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')
⊢ β fs
have rw : β
  (splitFun (α := v ::: t) (α' := v' ::: t') (dropFun (α := v ::: t) (β := v' ::: t') fs)
    (lastFun (α := v ::: t) (β := v' ::: t') fs))
Tactic: rw [← split_dropFun_lastFun fs]
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) = appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) fun (x_1 : β) ↦ x
have a : ∀ (i : Fin2 (n + 1)),
  TypeVec.const x (α ::: β) i = appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) i
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) i
have 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)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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)
⊢ TypeVec.const x (α ::: β) i = appendFun (α := α) (α' := «repeat» n γ) (TypeVec.const x α) (fun (x_1 : β) ↦ x) i
have 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)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
⊢ f = nilFun (α := α) (β := β)
have a : ∀ (x : Fin2 0) (x_1 : α x), f x x_1 = nilFun (α := α) (β := β) x x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
α : TypeVec.{u_1} 0
⊢ Eq.{u_1 + 1} (α := α ⟹ α) (id (α := α)) (nilFun (α := α) (β := α))
have a : ∀ (x : Fin2 0) (x_1 : α x), id (α := α) x x_1 = nilFun (α := α) (β := α) x x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
β : Type u_1
x : β
α : TypeVec.{u_2} 0
⊢ TypeVec.const x α = nilFun (α := α) (β := «repeat» 0 β)
have a : ∀ (i : Fin2 0), TypeVec.const x α i = nilFun (α := α) (β := «repeat» 0 β) i
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
β : Type u_1
n : ℕ
α : TypeVec.{u_1} n
⊢ (α ::: β).repeatEq =
    splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» n Prop ::: Prop) α.repeatEq
      (uncurry Eq)
have zero : ∀ (α : TypeVec.{u_1} 0),
  (α ::: β).repeatEq =
    splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» 0 Prop ::: Prop) α.repeatEq
      (uncurry Eq)
Tactic: induction n
Cleared hypotheses: n, α
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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)
⊢ (α ::: β).repeatEq =
    splitFun (α := (α ⊗ α) ::: ((α ::: β).last × (α ::: β).last)) (α' := «repeat» n Prop ::: Prop) α.repeatEq
      (uncurry Eq)
have 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)
Tactic: induction n
Cleared hypotheses: n, α
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
α : TypeVec.{u_1} 0
⊢ α.repeatEq = nilFun (α := α ⊗ α) (β := «repeat» 0 Prop)
have a : ∀ (i : Fin2 0) (x : (α ⊗ α) i), α.repeatEq i x = nilFun (α := α ⊗ α) (β := «repeat» 0 Prop) i x
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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 p α a.fs x) ↔ p
have fs : ofRepeat (TypeVec.const.{0, u_1} p α.drop a x) ↔ p
Tactic: rw [TypeVec.const]
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
p : Prop
⊢ ofRepeat (TypeVec.const p α i x) ↔ p
have fz : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {x : α Fin2.fz}, ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p
Tactic: induction i with
  | fz => rfl
  | fs _ ih =>
    rw [TypeVec.const]
    exact ih
Cleared hypotheses: α, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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
⊢ ofRepeat (TypeVec.const p α i x) ↔ p
have 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
Tactic: induction i with
  | fz => rfl
  | fs _ ih =>
    rw [TypeVec.const]
    exact ih
Cleared hypotheses: α, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.fst (α := α) (β := β) i (prod.mk (α := α) (β := β) i a b) = a
have fz : ∀ {n : ℕ} {α β : TypeVec.{u_1} (n + 1)} (a : α Fin2.fz) (b : β Fin2.fz),
  prod.fst (α := α) (β := β) Fin2.fz (prod.mk (α := α) (β := β) Fin2.fz a b) = a
Tactic: induction i with
  | fz => simp_all only [prod.fst, prod.mk]
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, β, i, a, b
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
fz :
  ∀ {n : ℕ} {α β : TypeVec.{u_1} (n + 1)} (a : α Fin2.fz) (b : β Fin2.fz),
    prod.fst (α := α) (β := β) Fin2.fz (prod.mk (α := α) (β := β) Fin2.fz a b) = a
⊢ prod.fst (α := α) (β := β) i (prod.mk (α := α) (β := β) i a b) = a
have fs : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α β : TypeVec.{u_1} n} (a_1 : α a) (b : β a),
      prod.fst (α := α) (β := β) a (prod.mk (α := α) (β := β) a a_1 b) = a_1)
  {α β : TypeVec.{u_1} (n + 1)} (a_1 : α a.fs) (b : β a.fs),
  prod.fst (α := α) (β := β) a.fs (prod.mk (α := α) (β := β) a.fs a_1 b) = a_1
Tactic: induction i with
  | fz => simp_all only [prod.fst, prod.mk]
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, β, i, a, b
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.snd (α := α) (β := β) i (prod.mk (α := α) (β := β) i a b) = b
have fz : ∀ {n : ℕ} {α β : TypeVec.{u_1} (n + 1)} (a : α Fin2.fz) (b : β Fin2.fz),
  prod.snd (α := α) (β := β) Fin2.fz (prod.mk (α := α) (β := β) Fin2.fz a b) = b
Tactic: induction i with
  | fz => simp_all [prod.snd, prod.mk]
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, β, i, a, b
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
fz :
  ∀ {n : ℕ} {α β : TypeVec.{u_1} (n + 1)} (a : α Fin2.fz) (b : β Fin2.fz),
    prod.snd (α := α) (β := β) Fin2.fz (prod.mk (α := α) (β := β) Fin2.fz a b) = b
⊢ prod.snd (α := α) (β := β) i (prod.mk (α := α) (β := β) i a b) = b
have fs : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α β : TypeVec.{u_1} n} (a_1 : α a) (b : β a),
      prod.snd (α := α) (β := β) a (prod.mk (α := α) (β := β) a a_1 b) = b)
  {α β : TypeVec.{u_1} (n + 1)} (a_1 : α a.fs) (b : β a.fs),
  prod.snd (α := α) (β := β) a.fs (prod.mk (α := α) (β := β) a.fs a_1 b) = b
Tactic: induction i with
  | fz => simp_all [prod.snd, prod.mk]
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, β, i, a, b
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) =
    comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α'))
have h : ∀ (i : Fin2 n),
  comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) i
have h : ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α ⟹ β) (g : α' ⟹ β'),
  Eq (α := (α ⊗ α') Fin2.fz → β Fin2.fz)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) Fin2.fz)
    (comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) Fin2.fz)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, α', β, β', f, g, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
h :
  ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α ⟹ β) (g : α' ⟹ β'),
    Eq (α := (α ⊗ α') Fin2.fz → β Fin2.fz)
      (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
        (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) Fin2.fz)
      (comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) Fin2.fz)
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) i
have h₁ : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α α' β β' : TypeVec.{u_1} n} (f : α ⟹ β) (g : α' ⟹ β'),
      comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
          (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a =
        comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) a)
  {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α ⟹ β) (g : α' ⟹ β'),
  Eq (α := (α ⊗ α') a.fs → β a.fs)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a.fs)
    (comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) a.fs)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, α', β, β', f, g, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) =
    comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α'))
have h : ∀ (i : Fin2 n),
  comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) i
have h : ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α ⟹ β) (g : α' ⟹ β'),
  Eq (α := (α ⊗ α') Fin2.fz → β' Fin2.fz)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) Fin2.fz)
    (comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) Fin2.fz)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, α', β, β', f, g, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
h :
  ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α ⟹ β) (g : α' ⟹ β'),
    Eq (α := (α ⊗ α') Fin2.fz → β' Fin2.fz)
      (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
        (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) Fin2.fz)
      (comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) Fin2.fz)
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) i
have h₁ : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α α' β β' : TypeVec.{u_1} n} (f : α ⟹ β) (g : α' ⟹ β'),
      comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
          (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a =
        comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) a)
  {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α ⟹ β) (g : α' ⟹ β'),
  Eq (α := (α ⊗ α') a.fs → β' a.fs)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a.fs)
    (comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) a.fs)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, α', β, β', f, g, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
⊢ Eq.{u_1 + 1} (α := α ⟹ α) (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)))
    (id (α := α))
have h : ∀ (i : Fin2 n),
  Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
have h : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)},
  Eq.{u_1 + 1} (α := α Fin2.fz → α Fin2.fz)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) Fin2.fz)
    (id (α := α) Fin2.fz)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
h :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)},
    Eq.{u_1 + 1} (α := α Fin2.fz → α Fin2.fz)
      (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) Fin2.fz)
      (id (α := α) Fin2.fz)
⊢ Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
have h₁ : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α : TypeVec.{u_1} n},
      Eq.{u_1 + 1} (α := α a → α a)
        (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) a) (id (α := α) a))
  {α : TypeVec.{u_1} (n + 1)},
  Eq.{u_1 + 1} (α := α a.fs → α a.fs)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) a.fs) (id (α := α) a.fs)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
⊢ Eq.{u_1 + 1} (α := α ⟹ α) (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)))
    (id (α := α))
have h : ∀ (i : Fin2 n),
  Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
have h : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)},
  Eq.{u_1 + 1} (α := α Fin2.fz → α Fin2.fz)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) Fin2.fz)
    (id (α := α) Fin2.fz)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
h :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)},
    Eq.{u_1 + 1} (α := α Fin2.fz → α Fin2.fz)
      (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) Fin2.fz)
      (id (α := α) Fin2.fz)
⊢ Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
have h₁ : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α : TypeVec.{u_1} n},
      Eq.{u_1 + 1} (α := α a → α a)
        (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) a) (id (α := α) a))
  {α : TypeVec.{u_1} (n + 1)},
  Eq.{u_1 + 1} (α := α a.fs → α a.fs)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) a.fs) (id (α := α) a.fs)
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x y : α i
⊢ ofRepeat (α.repeatEq i (prod.mk (α := α) (β := α) i x y)) ↔ x = y
have fz : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {x y : α Fin2.fz},
  ofRepeat (α.repeatEq Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz x y)) ↔ x = y
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih =>
    rw [repeatEq]
    exact i_ih
Cleared hypotheses: α, i, x, y
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x y : α i
fz :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {x y : α Fin2.fz},
    ofRepeat (α.repeatEq Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz x y)) ↔ x = y
⊢ ofRepeat (α.repeatEq i (prod.mk (α := α) (β := α) i x y)) ↔ x = y
have fs : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih : ∀ {α : TypeVec.{u_1} n} {x y : α a}, ofRepeat (α.repeatEq a (prod.mk (α := α) (β := α) a x y)) ↔ x = y)
  {α : TypeVec.{u_1} (n + 1)} {x y : α a.fs}, ofRepeat (α.repeatEq a.fs (prod.mk (α := α) (β := α) a.fs x y)) ↔ x = y
Tactic: induction i with
  | fz => rfl
  | fs _ i_ih =>
    rw [repeatEq]
    exact i_ih
Cleared hypotheses: α, i, x, y
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u} n
⊢ comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) =
    prod.diag (α := α)
have a : ∀ (i : Fin2 n) (x : α i),
  comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) i x =
    prod.diag (α := α) i x
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u} n
i : Fin2 n
x : α i
⊢ comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) i x =
    prod.diag (α := α) i x
have a : ∀ {n : ℕ} {α : TypeVec.{u} (n + 1)} (x : α Fin2.fz),
  comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) Fin2.fz x =
    prod.diag (α := α) Fin2.fz x
Tactic: induction i with
  | fz => simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]
  | fs _ i_ih => apply @i_ih (drop α)
Cleared hypotheses: α, i, x