-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
rw :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
rw₁ :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
            (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))))
rw₂ :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: β)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
            (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))))
rw₃ :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β)
            (comp (α := ((P F).B a).drop) (β := α) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
            (recF (F := F) (α := α) g ∘ f))))
⊢ recF (F := F) (α := α) g ((P F).wMk (α := α) a f' f) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
have rw₄ : g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
  g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f))))
Tactic: rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]