-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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'
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')
⊢ 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')

Tactic:
rw [Fix.rec_eq]

Premises used: MvQPF.Fix.rec_eq