[GOAL]
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F G : Prefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))
⊢ F = G
[PROOFSTEP]
cases' F with F_obj _
[GOAL]
case mk
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
G : Prefunctor V W
F_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝ }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝ }.map f =
      Eq.recOn (_ : G.obj Y = { obj := F_obj, map := map✝ }.obj Y)
        (Eq.recOn (_ : G.obj X = { obj := F_obj, map := map✝ }.obj X) (G.map f))
⊢ { obj := F_obj, map := map✝ } = G
[PROOFSTEP]
cases' G with G_obj _
[GOAL]
case mk.mk
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := G_obj, map := map✝ }.map f))
⊢ { obj := F_obj, map := map✝¹ } = { obj := G_obj, map := map✝ }
[PROOFSTEP]
obtain rfl : F_obj = G_obj := by
  ext X
  apply h_obj
[GOAL]
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := G_obj, map := map✝ }.map f))
⊢ F_obj = G_obj
[PROOFSTEP]
ext X
[GOAL]
case h
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := G_obj, map := map✝ }.map f))
X : V
⊢ F_obj X = G_obj X
[PROOFSTEP]
apply h_obj
[GOAL]
case mk.mk
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := F_obj, map := map✝ }.map f))
⊢ { obj := F_obj, map := map✝¹ } = { obj := F_obj, map := map✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_map
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := F_obj, map := map✝ }.map f))
⊢ map✝¹ = map✝
[PROOFSTEP]
funext X Y f
[GOAL]
case mk.mk.e_map.h.h.h
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := F_obj, map := map✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f
[PROOFSTEP]
simpa using h_map X Y f
