dsimp [Hom.mapEdgeSet]
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ mapEdgeSet f { val := e₁, property := h₁ } = mapEdgeSet f { val := e₂, property := h₂ } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ { val := (↑f e₁.fst, ↑f e₁.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₁, property := h₁ } ∈ edgeSet G') } =
      { val := (↑f e₂.fst, ↑f e₂.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₂, property := h₂ } ∈ edgeSet G') } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }