-- Module: Mathlib.Combinatorics.Quiver.Push
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X Y : V
f : X ⟶ Y
h_map :
  ∀ (h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)),
    Φ.map (PushQuiver.arrow f) =
      @Eq.recOn.{u_5 + 1, u_3 + 1} _ _
        (fun (x : W')
            (x_1 :
              Prefunctor.obj
                  { obj := Φ.obj,
                    map :=
                      @PushQuiver.rec V inst W σ
                        (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ Φ.obj X ⟶ Φ.obj Y)
                        fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) :
                    Push σ ⥤q W' }
                  (σ Y) =
                x) ↦
          Φ.obj (σ X) ⟶ x)
        (Φ.obj (σ Y)) ⋯
        (@Eq.recOn.{u_5 + 1, u_3 + 1} _ _
            (fun (x : W')
                (x_1 :
                  Prefunctor.obj
                      { obj := Φ.obj,
                        map :=
                          @PushQuiver.rec V inst W σ
                            (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ Φ.obj X ⟶ Φ.obj Y)
                            fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) :
                        Push σ ⥤q W' }
                      (σ X) =
                    x) ↦
              x ⟶
                Prefunctor.obj
                  { obj := Φ.obj,
                    map :=
                      @PushQuiver.rec V inst W σ
                        (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ Φ.obj X ⟶ Φ.obj Y)
                        fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) }
                  (σ Y))
            (Φ.obj (σ X)) ⋯
            (Prefunctor.map
                { obj := Φ.obj,
                  map :=
                    @PushQuiver.rec V inst W σ
                      (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ Φ.obj X ⟶ Φ.obj Y)
                      fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) }
                (PushQuiver.arrow f) :
              Prefunctor.obj
                  { obj := Φ.obj,
                    map :=
                      @PushQuiver.rec V inst W σ
                        (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ Φ.obj X ⟶ Φ.obj Y)
                        fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) :
                    Push σ ⥤q W' }
                  (σ X) ⟶
                Prefunctor.obj
                  { obj := Φ.obj,
                    map :=
                      @PushQuiver.rec V inst W σ
                        (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ Φ.obj X ⟶ Φ.obj Y)
                        fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) }
                  (σ Y)) :
          Φ.obj (σ X) ⟶
            Prefunctor.obj
              { obj := Φ.obj,
                map :=
                  @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ Φ.obj X ⟶ Φ.obj Y)
                    fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) }
              (σ Y))
⊢ Φ.map (PushQuiver.arrow f) =
    @Eq.recOn.{u_5 + 1, u_3 + 1} _ _
      (fun (x : W')
          (x_1 :
            Prefunctor.obj
                { obj := τ,
                  map :=
                    @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
                      fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) :
                  Push σ ⥤q W' }
                (σ Y) =
              x) ↦
        Φ.obj (σ X) ⟶ x)
      (Φ.obj (σ Y)) ⋯
      (@Eq.recOn.{u_5 + 1, u_3 + 1} _ _
          (fun (x : W')
              (x_1 :
                Prefunctor.obj
                    { obj := τ,
                      map :=
                        @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
                          fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) :
                      Push σ ⥤q W' }
                    (σ X) =
                  x) ↦
            x ⟶
              Prefunctor.obj
                { obj := τ,
                  map :=
                    @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
                      fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) }
                (σ Y))
          (Φ.obj (σ X)) ⋯
          (Prefunctor.map
              { obj := τ,
                map :=
                  @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
                    fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) }
              (PushQuiver.arrow f) :
            Prefunctor.obj
                { obj := τ,
                  map :=
                    @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
                      fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) :
                  Push σ ⥤q W' }
                (σ X) ⟶
              Prefunctor.obj
                { obj := τ,
                  map :=
                    @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
                      fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) }
                (σ Y)) :
        Φ.obj (σ X) ⟶
          Prefunctor.obj
            { obj := τ,
              map :=
                @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
                  fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) }
            (σ Y))

Tactic:
subst_vars