-- 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 ⟹ α))
h :
  ∀ (a : P.wp.A) (f : P.wp.B a ⟹ α),
    Eq (α := (↑P.wp : (α : TypeVec.{u} n) → Type u) β)
      (MvFunctor.map (F := (↑P.wp : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) g
        (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α) a f))
      (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β) a (TypeVec.comp (α := P.wp.B a) (β := α) (γ := β) g f))
rw :
  Eq (α := P.W β)
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
      (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (TypeVec.comp (α :=
        P.wp.B (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)))
        (β := α) (γ := β) g
        (P.wPathCasesOn (α := α) f' fun (i : P.last.B a) ↦ (f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
      (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.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 ⟹ α))))
⊢ Eq (α := P.W β)
    (MvFunctor.map (F := P.W) (α := α) (β := β) g
      (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α)
        (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
        (P.wPathCasesOn (α := α) f' fun (i : P.last.B a) ↦ (f i).snd (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))))
    (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
      (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
      (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.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 rw₁ : Eq (α := P.W β)
  (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
    (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
    (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.B a) ↦
      TypeVec.comp (α := P.WPath ((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 ⟹ α))))
  (Sigma.mk (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ β)
    (WType.mk (β := P.last.B) a fun (i : P.last.B a) ↦ (f i).fst (β := fun (a : P.wp.A) ↦ P.wp.B a ⟹ α))
    (P.wPathCasesOn (α := β) (TypeVec.comp (α := P.drop.B a) (β := α) (γ := β) g f') fun (i : P.last.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 [h, comp_wPathCasesOn]