-- 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 α
Hr : Relation.EqvGen R x y
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
refine_2 :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
          α ::: Quot (Relation.EqvGen R))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
          α ::: Quot (Relation.EqvGen R))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y)
refine_2₁ :
  ∀ (x : P.M α),
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
        α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
        α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x)
refine_2₂ :
  ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
            α ::: Quot (Relation.EqvGen R))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
          MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
            α ::: Quot (Relation.EqvGen R))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y) →
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
            α ::: Quot (Relation.EqvGen R))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y) =
          MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
            α ::: Quot (Relation.EqvGen R))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x)
refine_2₃ :
  ∀ (x y z : P.M α),
    Relation.EqvGen R x y →
      Relation.EqvGen R y z →
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
              α ::: Quot (Relation.EqvGen R))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
            MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
              α ::: Quot (Relation.EqvGen R))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y) →
          MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
                α ::: Quot (Relation.EqvGen R))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y) =
              MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
                α ::: Quot (Relation.EqvGen R))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) z) →
            MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
                α ::: Quot (Relation.EqvGen R))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
              MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
                α ::: Quot (Relation.EqvGen R))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) z)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y)

Tactic:
induction Hr