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

State before:
ι : Sort ?u.65081
𝕜 : Type ?u.65084
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 = deleteEdges G (s ∩ edgeSet G)
Tactic:
ext
State after:
case Adj.h.h.a
ι : Sort ?u.65081
𝕜 : Type ?u.65084
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)
x✝¹ x✝ : V
⊢ (deleteEdges G s).Adj x✝¹ x✝ ↔ (deleteEdges G (s ∩ edgeSet G)).Adj x✝¹ x✝

State before:
case Adj.h.h.a
ι : Sort ?u.65081
𝕜 : Type ?u.65084
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)
x✝¹ x✝ : V
⊢ (deleteEdges G s).Adj x✝¹ x✝ ↔ (deleteEdges G (s ∩ edgeSet G)).Adj x✝¹ x✝
Tactic:
simp (config := { contextual := true }) [imp_false]
State after:
no goals