-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
h₁ : ∀ (u v : (P F).M α), Mcongr (F := F) (α := α) u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (r := r) (Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α)) = Quot.mk r'
rw :
  MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (f ∘ Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (M.dest (P F) (α := α) a)) =
    MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (f ∘ Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (M.dest (P F) (α := α) b))
rw₁ :
  MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := α ::: Quot r')
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α)))))
        (M.dest (P F) (α := α) a)) =
    MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := α ::: Quot r')
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α)))))
        (M.dest (P F) (α := α) b))
rw₂ :
  MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
          (M.dest (P F) (α := α) a))) =
    MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := α ::: Quot r')
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α)))))
        (M.dest (P F) (α := α) b))
rw₃ :
  MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
          (M.dest (P F) (α := α) a))) =
    MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
          (M.dest (P F) (α := α) b)))
rw₄ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r') (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvQPF.abs (F := F) (α := α ::: Quot r)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
          (M.dest (P F) (α := α) a))) =
    MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
          (M.dest (P F) (α := α) b)))
rw₅ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r') (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a))) =
    MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
          (M.dest (P F) (α := α) b)))
rw₆ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r') (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a))) =
    MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvQPF.abs (F := F) (α := α ::: Quot r)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
          (M.dest (P F) (α := α) b)))
rw₇ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r') (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a))) =
    MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b)))
rw₈ rw₉ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r') (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))) =
    MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b)))
⊢ MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (M.dest (P F) (α := α) a)) =
    MvQPF.abs (F := F) (α := α ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := α ::: Quot r')
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (M.dest (P F) (α := α) b))

Tactic:
rw [← this, appendFun_comp_id, q.P.comp_map, q.P.comp_map, abs_map, abs_map, abs_map, abs_map,
      h₀]

Premises used: MvPFunctor.comp_map, MvQPF.abs_map, MvQPF.P, TypeVec.appendFun_comp_id