-- 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 Φ = φ
h_obj :
  ∀ (X : Push σ),
    Φ.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))) }
        X
h_map :
  ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map 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))) }
                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)
⊢ Φ =
    { 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))) }

Tactic:
fapply Prefunctor.ext

Premises used: Prefunctor.ext