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

State before:
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
⊢ edgeSet (deleteEdges G s) = edgeSet G \ s
Tactic:
ext e
State after:
case h
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
e : V × V
⊢ e ∈ edgeSet (deleteEdges G s) ↔ e ∈ edgeSet G \ s

State before:
case h
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
e : V × V
⊢ e ∈ edgeSet (deleteEdges G s) ↔ e ∈ edgeSet G \ s
Tactic:
cases e
State after:
case h.mk
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
fst✝ snd✝ : V
⊢ (fst✝, snd✝) ∈ edgeSet (deleteEdges G s) ↔ (fst✝, snd✝) ∈ edgeSet G \ s

State before:
case h.mk
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
fst✝ snd✝ : V
⊢ (fst✝, snd✝) ∈ edgeSet (deleteEdges G s) ↔ (fst✝, snd✝) ∈ edgeSet G \ s
Tactic:
simp
State after:
no goals