-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x_1 : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun (a b : Cofix F α) ↦
    ∃ (x : Cofix F α),
      a =
          corec (F := F) (α := α) (β := Cofix F α ⊕ β)
            (Function.comp (β := F (α ::: (Cofix F α ⊕ β)))
              (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
              (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
                (fun (val : Cofix F α) ↦
                  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
                fun (val : β) ↦ g val))
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec (F := F) (α := α) (β := Cofix F α ⊕ β)
      (Function.comp (β := F (α ::: (Cofix F α ⊕ β)))
        (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
        (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
          (fun (val : Cofix F α) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (Sum.inl x)
Hb : b = x
h :
  LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Function.comp (β := Cofix F α ⊕ β)
          (Function.comp (β := Cofix F α ⊕ β)
            (corec (F := F) (α := α) fun (x : Cofix F α ⊕ β) ↦
              MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x)
                (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
                  (fun (val : Cofix F α) ↦
                    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
                  (fun (val : β) ↦ g val) x))
            fun (x : Cofix F α ⊕ β) ↦ x)
          Sum.inl))
      (x.dest (F := F) (α := α)))
    (x.dest (F := F) (α := α))
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α) fun (x : Cofix F α ⊕ β) ↦
          MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x)
            (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
              (fun (val : Cofix F α) ↦
                MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
              (fun (val : β) ↦ g val) x)))
      (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x)
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (x.dest (F := F) (α := α)))))
    (x.dest (F := F) (α := α))

Tactic:
repeat rw [MvFunctor.map_map, ← appendFun_comp_id]

Premises used: TypeVec.appendFun_comp_id, MvFunctor.map_map