-- 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 Φ = φ
X Y : V
f : X ⟶ 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))
have 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 (sorry.mpr (sorry.mpr ((of σ ⋙q Φ).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 := Φ.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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.mpr ((of σ ⋙q Φ).map f))) }
                (σ Y))
          (Φ.obj (σ X)) sorry
          (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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.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 (sorry.mpr (sorry.mpr ((of σ ⋙q Φ).map f))) }
            (σ Y))
Tactic: subst_vars
Cleared hypotheses: φ, τ, h, Φ₀, Φcomp