-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id
rw :
  dest (F := F) (α := α)
      (corec (F := F) (α := α)
        (fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
        x) =
    x
rw₁ :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    x
rw₂ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₃ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α)) (γ := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (mk (F := F) (α := α)))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₄ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α)
        (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α)))
        (mk (F := F) (α := α) ∘ fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
      x =
    x
rw₅ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α)
        (TypeVec.comp (α := α) (β := α) (γ := α) (TypeVec.id (α := α)) (TypeVec.id (α := α))) _root_.id)
      x =
    x
rw₆ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x =
    x
⊢ (mk (F := F) (α := α) x).dest (F := F) (α := α) = x
have rw₇ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α) (TypeVec.id (α := α ::: Cofix F α)) x = x
Tactic: rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]