-- Mathlib/Combinatorics/Quiver/Prefunctor.lean
theorem ext' {V W : Type u} [Quiver V] [Quiver W] {F G : Prefunctor 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:
case mk.mk.h.h.h
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
X Y : V
f : X ⟶ Y
⊢ Fmap f = Gmap f

Tactic:
simpa only [Quiver.homOfEq_rfl] using h_map X Y f

Result:
no goals

Proof state:
case mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
G : Prefunctor V W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = G

Tactic:
obtain ⟨Gobj, Gmap⟩ := G

Result:
case mk.mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
Gobj : V → W
Gmap : {X Y : V} → (X ⟶ Y) → (Gobj X ⟶ Gobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Gobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Gobj, map := Gmap }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = { obj := Gobj, map := Gmap }

Proof state:
case mk.mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = { obj := Fobj, map := Gmap }

Tactic:
simp only [mk.injEq, heq_eq_eq, true_and]

Result:
case mk.mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
⊢ Fmap = Gmap

Proof state:
case mk.mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
Gobj : V → W
Gmap : {X Y : V} → (X ⟶ Y) → (Gobj X ⟶ Gobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Gobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Gobj, map := Gmap }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = { obj := Gobj, map := Gmap }

Tactic:
obtain rfl : Fobj = Gobj := funext h_obj

Result:
case mk.mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = { obj := Fobj, map := Gmap }

Proof state:
V W : Type u
inst✝¹ : Quiver V
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 = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ F = G

Tactic:
obtain ⟨Fobj, Fmap⟩ := F

Result:
case mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
G : Prefunctor V W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = G

Proof state:
case mk.mk
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
⊢ Fmap = Gmap

Tactic:
ext X Y f

Result:
case mk.mk.h.h.h
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
X Y : V
f : X ⟶ Y
⊢ Fmap f = Gmap f