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

State before:
ι : Sort ?u.70267
𝕜 : Type ?u.70270
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
⊢ Monotone (Digraph.comap f)
Tactic:
intro G G' h _ _ ha
State after:
ι : Sort ?u.70267
𝕜 : Type ?u.70270
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 W
h : G ≤ G'
v✝ w✝ : V
ha : (Digraph.comap f G).Adj v✝ w✝
⊢ (Digraph.comap f G').Adj v✝ w✝

State before:
ι : Sort ?u.70267
𝕜 : Type ?u.70270
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 W
h : G ≤ G'
v✝ w✝ : V
ha : (Digraph.comap f G).Adj v✝ w✝
⊢ (Digraph.comap f G').Adj v✝ w✝
Tactic:
exact h ha
State after:
no goals