-- 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
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'
⊢ Eq (α := F (α ::: Fix F α))
    (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β)))
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Sigma β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i)))
        x'))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x')
have e_x : Eq (α := F (α ::: Fix F α))
  (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (Function.comp (β := Sigma β) (Sigma.fst (β := β))
        (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
          Sigma.mk (β := β)
            (mk (F := F) (α := α)
              (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
            (g i))))
    x')
  (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
      Sigma.fst (β := β)
        (rec (F := F) (α := α)
          (fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i))
          x))
    x')
Tactic: rw [MvFunctor.map_map, ← appendFun_comp, id_comp]