awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h :
  ∀ (x : P.M α),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := β) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
e_a :
  lastFun (α := α ::: P.M α) (β := β ::: P.M β) g =
    lastFun (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := (α ::: P.M α).drop) (α' := (β ::: P.M β).drop) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g)
        fun (x : P.M (α ::: P.M α).drop) ↦
        MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
          (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x)
⊢ g =
    appendFun (α := (α ::: P.M α).drop) (α' := (β ::: P.M β).drop) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g)
      fun (x : P.M (α ::: P.M α).drop) ↦
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
        (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x

Tactic:
apply eq_of_drop_last_eq (by simp)

Premises used: TypeVec.eq_of_drop_last_eq
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h :
  ∀ (x : P.M α),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := β) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
e_a :
  lastFun (α := α ::: P.M α) (β := β ::: P.M β) g = fun (x : P.M (α ::: P.M α).drop) ↦
    MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
      (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
⊢ lastFun (α := α ::: P.M α) (β := β ::: P.M β) g =
    lastFun (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := (α ::: P.M α).drop) (α' := (β ::: P.M β).drop) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g)
        fun (x : P.M (α ::: P.M α).drop) ↦
        MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
          (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x)

Tactic:
simp only [lastFun_appendFun]

Premises used: TypeVec.lastFun_appendFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h :
  ∀ (x : P.M α),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := β) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
e_a :
  ∀ (x : (α ::: P.M α).last),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
        (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
⊢ lastFun (α := α ::: P.M α) (β := β ::: P.M β) g = fun (x : P.M (α ::: P.M α).drop) ↦
    MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
      (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x

Tactic:
ext1
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h :
  ∀ (x : P.M α),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := β) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
x_1 : (α ::: P.M α).last
⊢ lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x_1 =
    MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
      (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x_1

Tactic:
apply h
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i_1 : Fin2 n
x : P.WPath (WType.mk (β := P.last.B) a f) i_1
i : Fin2 n
c : P.drop.B a i
⊢ α i

Tactic:
exact g' i c
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i_1 : Fin2 n
x : P.WPath (WType.mk (β := P.last.B) a f) i_1
i : Fin2 n
j : P.last.B a
c : P.WPath (f j) i
⊢ α i

Tactic:
exact g j i c
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk (β := P.last.B) a f) i
⊢ α i

Tactic:
match x with
  | WPath.root _ _ i c => exact g' i c
  | WPath.child _ _ i j c => exact g j i c
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ P.wPathDestLeft (α := α) (P.wPathCasesOn (α := α) g' g) = g'

Tactic:
rfl

Premises used: MvPFunctor.wPathDestLeft, MvPFunctor.wPathCasesOn, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ P.wPathDestRight (α := α) (P.wPathCasesOn (α := α) g' g) = g

Tactic:
rfl

Premises used: MvPFunctor.wPathCasesOn, MvPFunctor.wPathDestRight, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk (β := P.last.B) a f) ⟹ α
a₁ :
  ∀ (i : Fin2 n) (x : P.WPath (WType.mk (β := P.last.B) a f) i),
    P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i x = h i x
⊢ P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) = h

Tactic:
ext i x
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk (β := P.last.B) a f) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk (β := P.last.B) a f) i
a₁ :
  ∀ (c : P.drop.B a i),
    P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i (WPath.root a f i c) =
      h i (WPath.root a f i c)
a₂ :
  ∀ (j : P.last.B a) (c : P.WPath (f j) i),
    P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i (WPath.child a f i j c) =
      h i (WPath.child a f i j c)
⊢ P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i x = h i x

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk (β := P.last.B) a f) ⟹ α
i : Fin2 n
c : P.drop.B a i
⊢ P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i (WPath.root a f i c) =
    h i (WPath.root a f i c)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk (β := P.last.B) a f) ⟹ α
i : Fin2 n
j : P.last.B a
c : P.WPath (f j) i
⊢ P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i (WPath.child a f i j c) =
    h i (WPath.child a f i j c)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
a₁ :
  ∀ (i : Fin2 n) (x : P.WPath (WType.mk (β := P.last.B) a f) i),
    TypeVec.comp (α := P.WPath (WType.mk (β := P.last.B) a f)) (β := α) (γ := β) h (P.wPathCasesOn (α := α) g' g) i x =
      P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) h g')
        (fun (i : P.last.B a) ↦ TypeVec.comp (α := P.WPath (f i)) (β := α) (γ := β) h (g i)) i x
⊢ TypeVec.comp (α := P.WPath (WType.mk (β := P.last.B) a f)) (β := α) (γ := β) h (P.wPathCasesOn (α := α) g' g) =
    P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) h g') fun (i : P.last.B a) ↦
      TypeVec.comp (α := P.WPath (f i)) (β := α) (γ := β) h (g i)

Tactic:
ext i x
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk (β := P.last.B) a f) i
a₁ :
  ∀ (c : P.drop.B a i),
    TypeVec.comp (α := P.WPath (WType.mk (β := P.last.B) a f)) (β := α) (γ := β) h (P.wPathCasesOn (α := α) g' g) i
        (WPath.root a f i c) =
      P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) h g')
        (fun (i : P.last.B a) ↦ TypeVec.comp (α := P.WPath (f i)) (β := α) (γ := β) h (g i)) i (WPath.root a f i c)
a₂ :
  ∀ (j : P.last.B a) (c : P.WPath (f j) i),
    TypeVec.comp (α := P.WPath (WType.mk (β := P.last.B) a f)) (β := α) (γ := β) h (P.wPathCasesOn (α := α) g' g) i
        (WPath.child a f i j c) =
      P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) h g')
        (fun (i : P.last.B a) ↦ TypeVec.comp (α := P.WPath (f i)) (β := α) (γ := β) h (g i)) i (WPath.child a f i j c)
⊢ TypeVec.comp (α := P.WPath (WType.mk (β := P.last.B) a f)) (β := α) (γ := β) h (P.wPathCasesOn (α := α) g' g) i x =
    P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) h g')
      (fun (i : P.last.B a) ↦ TypeVec.comp (α := P.WPath (f i)) (β := α) (γ := β) h (g i)) i x

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
c : P.drop.B a i
⊢ TypeVec.comp (α := P.WPath (WType.mk (β := P.last.B) a f)) (β := α) (γ := β) h (P.wPathCasesOn (α := α) g' g) i
      (WPath.root a f i c) =
    P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) h g')
      (fun (i : P.last.B a) ↦ TypeVec.comp (α := P.WPath (f i)) (β := α) (γ := β) h (g i)) i (WPath.root a f i c)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
j : P.last.B a
c : P.WPath (f j) i
⊢ TypeVec.comp (α := P.WPath (WType.mk (β := P.last.B) a f)) (β := α) (γ := β) h (P.wPathCasesOn (α := α) g' g) i
      (WPath.child a f i j c) =
    P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) h g')
      (fun (i : P.last.B a) ↦ TypeVec.comp (α := P.WPath (f i)) (β := α) (γ := β) h (g i)) i (WPath.child a f i j c)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
⊢ MvFunctor (n := n) fun (α : TypeVec.{u} n) ↦ (↑P.wp : (α : TypeVec.{u} n) → Type u) α

Tactic:
infer_instance
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_2} n
C : Sort u_1
g : (a : P.A) → (f : P.last.B a → P.last.W) → P.WPath (WType.mk (β := P.last.B) a f) ⟹ α → (P.last.B a → C) → C
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk (β := P.last.B) a f) ⟹ α
⊢ P.wpRec (α := α) g (WType.mk (β := P.last.B) a f) f' =
    g a f f' fun (i : P.last.B a) ↦ P.wpRec (α := α) g (f i) (P.wPathDestRight (α := α) f' i)

Tactic:
rfl

Premises used: MvPFunctor.wpRec, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : Sort u_1
g : (a : P.A) → P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ P.wRec (α := α) g (P.wMk (α := α) a f' f) = g a f' f fun (i : P.last.B a) ↦ P.wRec (α := α) g (f i)

Tactic:
rfl

Premises used: MvPFunctor.Obj, MvPFunctor.wPathDestLeft, MvPFunctor.wPathCasesOn, MvPFunctor.wPathDestRight, MvPFunctor.wRec, MvPFunctor.wpRec, MvPFunctor.W, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Sort v
ih :
  (a : P.A) →
    (f' : P.drop.B a ⟹ α) → (f : P.last.B a → P.W α) → ((i : P.last.B a) → C (f i)) → C (P.wMk (α := α) a f' f)
a : P.drop.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ P.wInd (α := α) (C := fun (x : P.W α) ↦ C x) ih (P.wMk (α := α) a f' f) =
    ih a f' f fun (i : P.last.B a) ↦ P.wInd (α := α) (C := fun (x : P.W α) ↦ C x) ih (f i)

Tactic:
rfl

Premises used: MvPFunctor.Obj, MvPFunctor.wPathDestLeft, cast, MvPFunctor.wPathCasesOn, MvPFunctor.wPathDestRight, MvPFunctor.wInd, MvPFunctor.wpInd, MvPFunctor.W, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ (P.wMk (α := α) a g' fun (i : P.last.B a) ↦ Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (f i) (g i)) =
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (WType.mk (β := P.last.B) a f) (P.wPathCasesOn (α := α) g' g)

Tactic:
rfl

Premises used: MvPFunctor.wMk, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
h :
  ∀ (i : P.last.B a),
    (MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f) i =
      Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
        (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
          ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
⊢ MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))

Tactic:
ext i : 1
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
i : P.last.B a
h :
  ∀ (fst : P.wp.A) (snd : P.wp.B fst ⟹ α),
    Eq (α := P.W β)
      (MvFunctor.map (F := P.W) (α := α) (β := β) g (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))
      (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
        (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))
        (TypeVec.comp (α :=
          P.wp.B
            (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
              (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd)))
          (β := α) (γ := β) g
          (Sigma.snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))))
⊢ MvFunctor.map (F := P.W) (α := α) (β := β) g (f i) =
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))

Tactic:
cases f i
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
i : P.last.B a
fst : P.wp.A
snd : P.wp.B fst ⟹ α
⊢ Eq (α := P.W β)
    (MvFunctor.map (F := P.W) (α := α) (β := β) g (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
      (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))
      (TypeVec.comp (α :=
        P.wp.B
          (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd)))
        (β := α) (γ := β) g
        (Sigma.snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))))

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))

Tactic:
have : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩ := by
    ext i : 1
    dsimp [Function.comp_def]
    cases f i
    rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
rw :
  MvFunctor.map (F := P.W) (α := α) (β := β) g (P.wMk (α := α) a f' f) =
    P.wMk (α := β) a (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.B a) ↦
      Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
        (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
          ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
⊢ MvFunctor.map (F := P.W) (α := α) (β := β) g (P.wMk (α := α) a f' f) =
    P.wMk (α := β) a (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f')
      (MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f)

Tactic:
rw [this]
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
h :
  ∀ (x : P.last.B a),
    f x =
      Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f x).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
        ((f x).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
⊢ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))

Tactic:
ext1 x
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
x : P.last.B a
h :
  ∀ (fst : P.wp.A) (snd : P.wp.B fst ⟹ α),
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd =
      Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
        (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))
        (Sigma.snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))
⊢ f x =
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f x).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      ((f x).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))

Tactic:
cases f x
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
x : P.last.B a
fst : P.wp.A
snd : P.wp.B fst ⟹ α
⊢ Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd =
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
      (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))
      (Sigma.snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) fst snd))

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.W
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this :
  MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α := P.wp.B ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))) (β := α) (γ := β) g
        ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
⊢ f = fun (i : P.last.B a) ↦
    Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) ((f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      ((f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))

Tactic:
have : f = fun i => ⟨(f i).fst, (f i).snd⟩ := by
    ext1 x
    cases f x
    rfl