exact h ha
case intro.intro.intro.intro
ι : Sort ?u.118218
𝕜 : Type ?u.118221
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 : Digraph V
G' : Digraph W
h : G ≤ Digraph.comap (↑f) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj (↑f u) (↑f v)
no goals