-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
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))
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) ⋯
            (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) ⋯
              ({ 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 }
⊢ { 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 }

Tactic:
obtain rfl : F_obj = G_obj := (Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _

Premises used: Set.eqOn_univ, Iff.mp, rfl