awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
have conv : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (β ::: P.M β))
  (dest P (α := β)
    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β ::: P.M β)
    ((PFunctor.M.dest
          (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
      (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))
    (splitFun (α :=
      P.B
        ((PFunctor.M.dest
              (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
          (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M)))
      (α' := β ::: P.M β)
      (TypeVec.comp (α :=
        (P.B
            ((PFunctor.M.dest
                  (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
              (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).drop)
        (β := α) (γ := (β ::: P.M β).drop) g
        (pathDestLeft P (α := (α ::: P.M α).drop) sorry
          (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))))
      ((fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x) ∘
        fun
          (x :
            (P.B
                ((PFunctor.M.dest
                      (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                        (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                  (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).last) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
          ((PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).snd
            (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M) x)
          (pathDestRight P (α := α) sorry
            (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
            x))))
Tactic: conv =>
    rhs
    rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
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
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β) g
      (dest P (α := α) x) =
    dest P (α := (β ::: P.M β).drop)
      (MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
        (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x)
have rw : MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β) g
    (dest P (α := α) x) =
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := (α ::: P.M α).drop ::: P.M (α ::: P.M α).drop)
    (β := (β ::: P.M β).drop ::: P.M (β ::: P.M β).drop)
    (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)
    (dest P (α := (α ::: P.M α).drop) x)
Tactic: rw [M.dest_map]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
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
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β) g
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := (α ::: P.M α).drop ::: P.M (α ::: P.M α).drop)
      (β := (β ::: P.M β).drop ::: P.M (β ::: P.M β).drop)
      (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)
      (dest P (α := (α ::: P.M α).drop) x)
have e_a : 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: congr
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
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
⊢ 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
have 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)
Tactic: apply eq_of_drop_last_eq (by simp)
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
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
⊢ 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)
have 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
Tactic: simp only [lastFun_appendFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
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
⊢ 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
have 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
Tactic: ext1
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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) ⟹ α
⊢ P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) = h
have 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
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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
⊢ P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i x = h i x
have 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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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)
⊢ P.wPathCasesOn (α := α) (P.wPathDestLeft (α := α) h) (P.wPathDestRight (α := α) h) i x = h i x
have 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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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) ⟹ α
⊢ 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)
have 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
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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
⊢ 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
have 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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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)
⊢ 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
have 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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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 ⟹ α)))
have 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 ⟹ α)))
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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
⊢ 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 ⟹ α)))
have 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))))
Tactic: cases f i
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (hypothesis)
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 (P.wMk (α := α) a f' f) =
    P.wMk (α := β) a (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f')
      (MvFunctor.map (F := P.W) (α := α) (β := β) g ∘ f)
have 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 ⟹ α)))
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
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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 ⟹ α)))
⊢ 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)
have 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 ⟹ α)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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 ⟹ α))
have 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 ⟹ α))
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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
⊢ 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 ⟹ α))
have 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))
Tactic: cases f x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (hypothesis)
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 ⟹ α)))
⊢ 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 ⟹ α)))
have this₁ : 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
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.W (goal)
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_1 :
  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 ⟹ α)))
this :
  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 ⟹ α))
⊢ MvFunctor.map (F := P.W) (α := α) (β := β) g
      (P.wMk (α := α) 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 ⟹ α))) =
    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 ⟹ β)
        (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
          ((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 ⟹ α)) :
                (a : P.wp.A) × P.wp.B a ⟹ α))
            i))
        (TypeVec.comp (α :=
          P.wp.B
            (Sigma.fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
              ((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 ⟹ α)) :
                    (a : P.wp.A) × P.wp.B a ⟹ α))
                i)))
          (β := α) (γ := β) g
          (Sigma.snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
            ((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 ⟹ α)) :
                  (a : P.wp.A) × P.wp.B a ⟹ α))
              i)))
have dsimp : MvFunctor.map (F := P.W) (α := α) (β := β) g
    (P.wMk (α := α) 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 ⟹ α))) =
  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 ⟹ α)))
Tactic: dsimp