-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
hu : (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
h :
  abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
        (appendFun (α := α) (α' := β) g u)
        (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₁))) =
    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 (α := α) (α' := β) g u)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
        (M.dest (P F) (α := α) a₂))
h₁ :
  abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
        (appendFun (α := α) (α' := β) g u)
        (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₁))) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
        (appendFun (α := α) (α' := β) g u)
        (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₂)))
h₂ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
      (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₁))) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
        (appendFun (α := α) (α' := β) g u)
        (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₂)))
h₃ :
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
      (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₂))) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
        (appendFun (α := α) (α' := β) g u)
        (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₂)))
h₄ h₅ :
  abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
        (appendFun (α := α) (α' := β) g u)
        (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₂))) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot r) (β := β ::: Quot r')
        (appendFun (α := α) (α' := β) g u)
        (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₂)))
⊢ 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 (α := α) (α' := β) g u)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
        (M.dest (P F) (α := α) a₁)) =
    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 (α := α) (α' := β) g u)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
        (M.dest (P F) (α := α) a₂))

Tactic:
rw [q.P.comp_map, q.P.comp_map, abs_map, pr ra₁a₂, ← abs_map]

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