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

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

State before:
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)
Tactic:
exact ⟨_, _, h ha, rfl, rfl⟩
State after:
no goals