-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
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
⊢ Φ =
    { 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))) }
have 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 (sorry.mpr (sorry.mpr (φ.map f))) :
                  Push σ ⥤q W' }
                Y =
              x) ↦
        Φ.obj X ⟶ x)
      (Φ.obj Y) sorry
      (@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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.mpr (φ.map f))) }
                Y)
          (Φ.obj X) sorry
          (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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.mpr (φ.map f))) }
            Y)
Tactic: fapply Prefunctor.ext