-- 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' =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x'
⊢ 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))
        (mk (F := F) (α := α) x')) =
    _root_.id (mk (F := F) (α := α) x')
have rw : (Sigma.mk (β := β)
        (mk (F := 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')))
        (g
          (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'))).fst
    (β := β) =
  _root_.id (mk (F := F) (α := α) x')
Tactic: rw [Fix.rec_eq]