-- Mathlib/Combinatorics/Quiver/ReflQuiver.lean
theorem ext' {V W : Type u} [ReflQuiver.{v} V] [ReflQuiver.{v} W]
    {F G : ReflPrefunctor V W}
    (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ (X Y : V) (f : X ⟶ Y),
      F.map f = Quiver.homOfEq (G.map f) (h_obj _).symm (h_obj _).symm) : F = G

Proof state:
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
F G : ReflPrefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ F = G

Tactic:
obtain ⟨Fpre, Fid⟩ := F

Result:
case mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
G : ReflPrefunctor V W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = G

Proof state:
case mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
G : ReflPrefunctor V W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = G

Tactic:
obtain ⟨Gpre, Gid⟩ := G

Result:
case mk.mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
Gpre : V ⥤q W
Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = { toPrefunctor := Gpre, map_id := Gid }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq ({ toPrefunctor := Gpre, map_id := Gid }.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Gpre, map_id := Gid }

Proof state:
case mk.mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
Gpre : V ⥤q W
Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = { toPrefunctor := Gpre, map_id := Gid }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq ({ toPrefunctor := Gpre, map_id := Gid }.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Gpre, map_id := Gid }

Tactic:
simp at h_obj h_map

Result:
case mk.mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
Gpre : V ⥤q W
Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X)
h_obj : ∀ (X : V), Fpre.obj X = Gpre.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), Fpre.map f = Quiver.homOfEq (Gpre.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Gpre, map_id := Gid }

Proof state:
case mk.mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
Gpre : V ⥤q W
Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X)
h_obj : ∀ (X : V), Fpre.obj X = Gpre.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), Fpre.map f = Quiver.homOfEq (Gpre.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Gpre, map_id := Gid }

Tactic:
obtain rfl : Fpre = Gpre := Prefunctor.ext' (V := V) (W := W) h_obj h_map

Result:
case mk.mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid Gid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), Fpre.obj X = Fpre.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), Fpre.map f = Quiver.homOfEq (Fpre.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Fpre, map_id := Gid }

Proof state:
case mk.mk
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid Gid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), Fpre.obj X = Fpre.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), Fpre.map f = Quiver.homOfEq (Fpre.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Fpre, map_id := Gid }

Tactic:
rfl

Result:
no goals