simp
case mk.mk.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
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝¹, snd✝¹).fst, ↑f (fst✝¹, snd✝¹).snd) = (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) →
    (fst✝¹, snd✝¹) = (fst✝, snd✝)
case mk.mk.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
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ ↑f fst✝¹ = ↑f fst✝ → ↑f snd✝¹ = ↑f snd✝ → fst✝¹ = fst✝ ∧ snd✝¹ = snd✝