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

State before:
ι : Sort ?u.62316
𝕜 : Type ?u.62319
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
⊢ deleteEdges G s ≤ G
Tactic:
intro
State after:
ι : Sort ?u.62316
𝕜 : Type ?u.62319
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
v✝ : V
⊢ ∀ ⦃w : V⦄, (deleteEdges G s).Adj v✝ w → G.Adj v✝ w

State before:
ι : Sort ?u.62316
𝕜 : Type ?u.62319
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
v✝ : V
⊢ ∀ ⦃w : V⦄, (deleteEdges G s).Adj v✝ w → G.Adj v✝ w
Tactic:
simp (config := { contextual := true })
State after:
no goals