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

State before:
ι : Sort ?u.64664
𝕜 : Type ?u.64667
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
s s' : Set (V × V)
h : s ⊆ s'
v w : V
⊢ (deleteEdges G s').Adj v w → (deleteEdges G s).Adj v w
Tactic:
simp (config := { contextual := true }) only [deleteEdges_adj, and_imp, true_and_iff]
State after:
ι : Sort ?u.64664
𝕜 : Type ?u.64667
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
s s' : Set (V × V)
h : s ⊆ s'
v w : V
⊢ G.Adj v w → ¬(v, w) ∈ s' → ¬(v, w) ∈ s

State before:
ι : Sort ?u.64664
𝕜 : Type ?u.64667
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
s s' : Set (V × V)
h : s ⊆ s'
v w : V
⊢ G.Adj v w → ¬(v, w) ∈ s' → ¬(v, w) ∈ s
Tactic:
exact fun _ hn hs => hn (h hs)
State after:
no goals