Theorem: Digraph.map_comap_le (GraphProjects/Digraph.lean)

State before:
ι : Sort ?u.133674
𝕜 : Type ?u.133677
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 W
⊢ Digraph.map (↑f) (Digraph.comap (↑f) G) ≤ G
Tactic:
rw [map_le_iff_le_comap]
State after:
no goals