-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
G_obj : V → W
map_1 : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 :
  ∀ (X : V),
    { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W)
          (x_1 : { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W)
            (x_1 : { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))
⊢ { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } =
    { obj := G_obj, map := @map_1, map_id := map_id_1 }
have obtain : ∀ (map_2 : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y))
  (map_id_2 :
    ∀ (X : V),
      { obj := F_obj, map := @map_2 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
        𝟙rq ({ obj := F_obj, map := @map_2 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X))
  (h_obj :
    ∀ (X : V),
      { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X =
        { obj := F_obj, map := @map_2, map_id := map_id_2 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X)
  (h_map :
    ∀ (X Y : V) (f : X ⟶ Y),
      { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f =
        Eq.recOn (motive :=
          fun (x : W)
            (x_1 : { obj := F_obj, map := @map_2, map_id := map_id_2 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
          { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) sorry
          (Eq.recOn (motive :=
            fun (x : W)
              (x_1 :
                { obj := F_obj, map := @map_2, map_id := map_id_2 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
            x ⟶ { obj := F_obj, map := @map_2, map_id := map_id_2 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) sorry
            ({ obj := F_obj, map := @map_2, map_id := map_id_2 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))),
  { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } =
    { obj := F_obj, map := @map_2, map_id := map_id_2 }
Tactic: obtain rfl : F_obj = G_obj := (Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _
Cleared hypotheses: G_obj, map_1, map_id_1, h_obj, h_map