-- 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 (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr (F := F) (α := α ::: Fix F α) x = Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f
rw :
  g
      (abs (F := F) (α := α ::: β)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: β)
          (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α))))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
rw₁ :
  g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α))))
        (abs (F := F) (α := α ::: Fix F α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
rw₂ :
  g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α))))
        (abs (F := F) (α := α ::: Fix F α) (repr (F := F) (α := α ::: Fix F α) x))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
rw₃ :
  g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α))))
        x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
⊢ g
      (abs (F := F) (α := α ::: β)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β :=
            α ::: (P F).W α) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f)))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
have rw₄ : g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
        (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)))
      x) =
  g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
Tactic: rw [← MvPFunctor.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]