awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.TypeVec
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
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
⊢ prod.fst (α := α) (β := β) i (prod.mk (α := α) (β := β) i a b) = a

Tactic:
induction i with
  | fz => simp_all only [prod.fst, prod.mk]
  | fs _ i_ih => apply i_ih

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

Tactic:
simp_all [prod.snd, prod.mk]

Premises used: TypeVec.prod.mk, TypeVec.prod.snd
-- 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.snd (α := α) (β := β) a_1 (prod.mk (α := α) (β := β) a_1 a b) = b
α β : TypeVec.{u_1} (n_1 + 1)
a : α a_1.fs
b : β a_1.fs
⊢ prod.snd (α := α) (β := β) a_1.fs (prod.mk (α := α) (β := β) a_1.fs a b) = b

Tactic:
apply i_ih
-- Module: Mathlib.Data.TypeVec
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
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
⊢ prod.snd (α := α) (β := β) i (prod.mk (α := α) (β := β) i a b) = b

Tactic:
induction i with
  | fz => simp_all [prod.snd, prod.mk]
  | fs _ i_ih => apply i_ih

Premises used: TypeVec.prod.mk, TypeVec.prod.snd
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
h :
  ∀ (i : Fin2 n),
    comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
        (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
      comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) i
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) =
    comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α'))

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α α' β β' : TypeVec.{u_1} (n_1 + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ Eq (α := (α ⊗ α') Fin2.fz → β Fin2.fz)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) Fin2.fz)
    (comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) Fin2.fz)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
i_ih :
  ∀ {α α' β β' : TypeVec.{u_1} n_1} (f : α ⟹ β) (g : α' ⟹ β'),
    comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
        (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a =
      comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) a
α α' β β' : TypeVec.{u_1} (n_1 + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ Eq (α := (α ⊗ α') a.fs → β a.fs)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a.fs)
    (comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) a.fs)

Tactic:
apply i_ih
-- Module: Mathlib.Data.TypeVec
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)
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)
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β) (prod.fst (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α) (γ := β) f (prod.fst (α := α) (β := α')) i

Tactic:
induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
h :
  ∀ (i : Fin2 n),
    comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
        (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
      comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) i
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) =
    comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α'))

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α α' β β' : TypeVec.{u_1} (n_1 + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ Eq (α := (α ⊗ α') Fin2.fz → β' Fin2.fz)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) Fin2.fz)
    (comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) Fin2.fz)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
i_ih :
  ∀ {α α' β β' : TypeVec.{u_1} n_1} (f : α ⟹ β) (g : α' ⟹ β'),
    comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
        (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a =
      comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) a
α α' β β' : TypeVec.{u_1} (n_1 + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ Eq (α := (α ⊗ α') a.fs → β' a.fs)
    (comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) a.fs)
    (comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) a.fs)

Tactic:
apply i_ih
-- Module: Mathlib.Data.TypeVec
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)
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)
⊢ comp (α := α ⊗ α') (β := β ⊗ β') (γ := β') (prod.snd (α := β) (β := β'))
      (prod.map (α := α) (α' := α') (β := β) (β' := β') f g) i =
    comp (α := α ⊗ α') (β := α') (γ := β') g (prod.snd (α := α) (β := α')) i

Tactic:
induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
h :
  ∀ (i : Fin2 n),
    Eq.{u_1 + 1} (α := α i → α i)
      (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
⊢ Eq.{u_1 + 1} (α := α ⟹ α) (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)))
    (id (α := α))

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
⊢ Eq.{u_1 + 1} (α := α Fin2.fz → α Fin2.fz)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) Fin2.fz)
    (id (α := α) Fin2.fz)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
i_ih :
  ∀ {α : TypeVec.{u_1} n_1},
    Eq.{u_1 + 1} (α := α a → α a)
      (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) a) (id (α := α) a)
α : TypeVec.{u_1} (n_1 + 1)
⊢ Eq.{u_1 + 1} (α := α a.fs → α a.fs)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) a.fs) (id (α := α) a.fs)

Tactic:
apply i_ih
-- Module: Mathlib.Data.TypeVec
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)
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)
⊢ Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)

Tactic:
induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
h :
  ∀ (i : Fin2 n),
    Eq.{u_1 + 1} (α := α i → α i)
      (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)
⊢ Eq.{u_1 + 1} (α := α ⟹ α) (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)))
    (id (α := α))

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
⊢ Eq.{u_1 + 1} (α := α Fin2.fz → α Fin2.fz)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) Fin2.fz)
    (id (α := α) Fin2.fz)

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
i_ih :
  ∀ {α : TypeVec.{u_1} n_1},
    Eq.{u_1 + 1} (α := α a → α a)
      (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) a) (id (α := α) a)
α : TypeVec.{u_1} (n_1 + 1)
⊢ Eq.{u_1 + 1} (α := α a.fs → α a.fs)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) a.fs) (id (α := α) a.fs)

Tactic:
apply i_ih
-- Module: Mathlib.Data.TypeVec
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)
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)
⊢ Eq.{u_1 + 1} (α := α i → α i)
    (comp (α := α) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α)) (prod.diag (α := α)) i) (id (α := α) i)

Tactic:
induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
x y : α Fin2.fz
⊢ ofRepeat (α.repeatEq Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz x y)) ↔ x = y

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
i_ih : ∀ {α : TypeVec.{u_1} n_1} {x y : α a}, ofRepeat (α.repeatEq a (prod.mk (α := α) (β := α) a x y)) ↔ x = y
α : TypeVec.{u_1} (n_1 + 1)
x y : α a.fs
⊢ ofRepeat
      (appendFun (α := α.drop ⊗ α.drop) (α' := «repeat» n_1 Prop) α.drop.repeatEq (uncurry Eq) a.fs
        (prod.mk (α := α) (β := α) a.fs x y)) ↔
    x = y

Tactic:
i_ih

Premises used: TypeVec.ofRepeat, TypeVec.prod.mk, TypeVec.appendFun, TypeVec.drop, TypeVec.splitFun
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
i_ih : ∀ {α : TypeVec.{u_1} n_1} {x y : α a}, ofRepeat (α.repeatEq a (prod.mk (α := α) (β := α) a x y)) ↔ x = y
α : TypeVec.{u_1} (n_1 + 1)
x y : α a.fs
⊢ ofRepeat
      (appendFun (α := α.drop ⊗ α.drop) (α' := «repeat» n_1 Prop) α.drop.repeatEq (uncurry Eq) a.fs
        (prod.mk (α := α) (β := α) a.fs x y)) ↔
    x = y

Tactic:
exact i_ih
-- Module: Mathlib.Data.TypeVec
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
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
⊢ ofRepeat (α.repeatEq i (prod.mk (α := α) (β := α) i x y)) ↔ x = y

Tactic:
induction i with
  | fz => rfl
  | fs _ i_ih =>
    rw [repeatEq]
    exact i_ih

Premises used: TypeVec.repeatEq
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
α_1 : TypeVec.{u} n
p_1 : α_1 ⊗ α_1 ⟹ «repeat» n Prop
n_2 : ℕ
α : TypeVec.{u} (n_2 + 1)
p : α ⊗ α ⟹ «repeat» (n_2 + 1) Prop
x : (fun (i : Fin2 (n_2 + 1)) ↦ { x : α i × α i // ofRepeat (p i (prod.mk (α := α) (β := α) i x.1 x.2)) }) Fin2.fz
⊢ ofRepeat
      (p Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz (↑x : α Fin2.fz × α Fin2.fz).1 (↑x : α Fin2.fz × α Fin2.fz).2)) =
    p Fin2.fz (↑x : α Fin2.fz × α Fin2.fz)

Tactic:
congr
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
α_1 : TypeVec.{u} n
p_1 : α_1 ⊗ α_1 ⟹ «repeat» n Prop
n_2 : ℕ
α : TypeVec.{u} (n_2 + 1)
p : α ⊗ α ⟹ «repeat» (n_2 + 1) Prop
x : Subtype_ (α := α ⊗ α) p Fin2.fz
⊢ p Fin2.fz (↑x : (α ⊗ α) Fin2.fz) =
    ofRepeat (p Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz (↑x : (α ⊗ α) Fin2.fz).1 (↑x : (α ⊗ α) Fin2.fz).2))

Tactic:
congr
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
a :
  ∀ (i : Fin2 n) (x : α i),
    comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
        (diagSub (α := α)) i x =
      prod.diag (α := α) i x
⊢ comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) =
    prod.diag (α := α)

Tactic:
ext i x
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u} (n_1 + 1)
x : α Fin2.fz
⊢ comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) Fin2.fz x =
    prod.diag (α := α) Fin2.fz x

Tactic:
simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]

Premises used: TypeVec.prod.diag, TypeVec.diagSub, TypeVec.comp, TypeVec.repeatEq.eq_2, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
i_ih :
  ∀ {α : TypeVec.{u} n_1} (x : α a),
    comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
        (diagSub (α := α)) a x =
      prod.diag (α := α) a x
α : TypeVec.{u} (n_1 + 1)
x : α a.fs
⊢ comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) a.fs x =
    prod.diag (α := α) a.fs x

Tactic:
apply @i_ih (drop α)
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
i : Fin2 n
x : α i
a :
  ∀ {n : ℕ} {α : TypeVec.{u} (n + 1)} (x : α Fin2.fz),
    comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
        (diagSub (α := α)) Fin2.fz x =
      prod.diag (α := α) Fin2.fz x
a₁ :
  ∀ {n : ℕ} (a : Fin2 n)
    (i_ih :
      ∀ {α : TypeVec.{u} n} (x : α a),
        comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
            (diagSub (α := α)) a x =
          prod.diag (α := α) a x)
    {α : TypeVec.{u} (n + 1)} (x : α a.fs),
    comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
        (diagSub (α := α)) a.fs x =
      prod.diag (α := α) a.fs x
⊢ comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) i x =
    prod.diag (α := α) i x

Tactic:
induction i with
  | fz => simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]
  | fs _ i_ih => apply @i_ih (drop α)

Premises used: TypeVec.prod.diag, TypeVec.diagSub, TypeVec.comp, TypeVec.repeatEq.eq_2, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α β : TypeVec.{u} n
a :
  ∀ (i : Fin2 n) (a : (α ⊗ β) i),
    prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) i a = id (α := α ⊗ β) i a
⊢ Eq.{u + 1} (α := α ⊗ β ⟹ α ⊗ β) (prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)))
    (id (α := α ⊗ β))

Tactic:
ext i a
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α β : TypeVec.{u} (n_1 + 1)
a : (α ⊗ β) Fin2.fz
a₁ :
  ∀ (fst : α.last) (snd : β.last),
    Eq.{u + 1} (α := (α ⊗ β) Fin2.fz)
      (prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz (fst, snd))
      (id (α := α ⊗ β) Fin2.fz (fst, snd))
⊢ prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz a = id (α := α ⊗ β) Fin2.fz a

Tactic:
cases a
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α β : TypeVec.{u} (n_1 + 1)
fst : α.last
snd : β.last
⊢ Eq.{u + 1} (α := (α ⊗ β) Fin2.fz)
    (prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz (fst, snd))
    (id (α := α ⊗ β) Fin2.fz (fst, snd))

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a_1 : Fin2 n_1
i_ih :
  ∀ {α β : TypeVec.{u} n_1} (a : (α ⊗ β) a_1),
    prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) a_1 a = id (α := α ⊗ β) a_1 a
α β : TypeVec.{u} (n_1 + 1)
a : (α ⊗ β) a_1.fs
⊢ prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) a_1.fs a = id (α := α ⊗ β) a_1.fs a

Tactic:
apply i_ih
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α β : TypeVec.{u} n
i : Fin2 n
a : (α ⊗ β) i
a₁ :
  ∀ {n : ℕ} {α β : TypeVec.{u} (n + 1)} (a : (α ⊗ β) Fin2.fz),
    prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz a = id (α := α ⊗ β) Fin2.fz a
a₂ :
  ∀ {n : ℕ} (a : Fin2 n)
    (i_ih :
      ∀ {α β : TypeVec.{u} n} (a_1 : (α ⊗ β) a),
        prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) a a_1 = id (α := α ⊗ β) a a_1)
    {α β : TypeVec.{u} (n + 1)} (a_1 : (α ⊗ β) a.fs),
    prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) a.fs a_1 = id (α := α ⊗ β) a.fs a_1
⊢ prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) i a = id (α := α ⊗ β) i a

Tactic:
induction i with
  | fz => cases a; rfl
  | fs _ i_ih => apply i_ih
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a :
  ∀ (i : Fin2 (n + 1)) (a : ((α ⊗ β) ::: (φ × ψ)) i),
    appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) i
        a =
      prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
        (appendFun (α := β) (α' := β') g₀ g₁) i a
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁)

Tactic:
ext i a
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
a₁ :
  ∀ (a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz),
    appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
        Fin2.fz a =
      prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
        (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz a
a₂ :
  ∀ (a : Fin2 n) (a_1 : ((α ⊗ β) ::: (φ × ψ)) a.fs),
    appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
        a.fs a_1 =
      prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
        (appendFun (α := β) (α' := β') g₀ g₁) a.fs a_1
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) i a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) i a

Tactic:
cases i
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
a₁ :
  ∀ (fst : φ) (snd : ψ),
    Eq (α := ((α' ⊗ β') ::: (φ' × ψ')) Fin2.fz)
      (appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
        Fin2.fz (fst, snd))
      (prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
        (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz (fst, snd))
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
      Fin2.fz a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz a

Tactic:
cases a
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
fst : φ
snd : ψ
⊢ Eq (α := ((α' ⊗ β') ::: (φ' × ψ')) Fin2.fz)
    (appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
      Fin2.fz (fst, snd))
    (prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz (fst, snd))

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a_1 : Fin2 n
a : ((α ⊗ β) ::: (φ × ψ)) a_1.fs
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
      a_1.fs a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) a_1.fs a

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ Eq.{u_1 + 1} (α := α.drop ⟹ (α ⊗ α).drop) (dropFun (α := α) (β := α ⊗ α) (prod.diag (α := α)))
    (prod.diag (α := α.drop))

Tactic:
rfl

Premises used: TypeVec.prod.diag, rfl, TypeVec.dropFun