exact ⟨_, _, h ha, rfl, rfl⟩
case intro.intro.intro.intro
ι : Sort ?u.69221
𝕜 : Type ?u.69224
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u✝ v✝ w : V
f : V → W
G G' : Digraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
⊢ (Digraph.map f G').Adj (f u) (f v)
no goals