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

State before:
ι : 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
⊢ G ≤ Digraph.comap (↑f) G' → Digraph.map (↑f) G ≤ G'
Tactic:
rintro h _ _ ⟨u, v, ha, rfl, rfl⟩
State after:
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)

State before:
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)
Tactic:
exact h ha
State after:
no goals