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

State before:
ι : Sort ?u.60271
𝕜 : Type ?u.60274
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
G G' : Digraph V
⊢ G \ G' = deleteEdges G (edgeSet G')
Tactic:
ext
State after:
case Adj.h.h.a
ι : Sort ?u.60271
𝕜 : Type ?u.60274
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
G G' : Digraph V
x✝¹ x✝ : V
⊢ (G \ G').Adj x✝¹ x✝ ↔ (deleteEdges G (edgeSet G')).Adj x✝¹ x✝

State before:
case Adj.h.h.a
ι : Sort ?u.60271
𝕜 : Type ?u.60274
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
G G' : Digraph V
x✝¹ x✝ : V
⊢ (G \ G').Adj x✝¹ x✝ ↔ (deleteEdges G (edgeSet G')).Adj x✝¹ x✝
Tactic:
simp
State after:
no goals