-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x_1 y_1 : P.M α
h_1 : R x_1 y_1
refine_2 :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
      (dest P (α := α) y_1)
refine_2₁ :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x_1)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
      (dest P (α := α) y_1)
refine_2₂ :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x_1)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y_1))
refine_2₃ :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y_1)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y_1))
refine_2₄ : P.M α
refine_2₅ : R x_1 y_1
refine_2₆ :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y_1)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y_1))
refine_2₇ : P.M α
refine_2₈ refine_2₉ refine_2₁₀ : R x_1 y_1
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R))
      (dest P (α := α) y_1)

Tactic:
rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]

Premises used: TypeVec.appendFun_comp_id, MvFunctor.map_map