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

State before:
ι : Sort ?u.55069
𝕜 : Type ?u.55072
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
⊢ edgeSet (G₁ \ G₂) = edgeSet G₁ \ edgeSet G₂
Tactic:
ext ⟨x, y⟩
State after:
case h.mk
ι : Sort ?u.55069
𝕜 : Type ?u.55072
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 y : V
⊢ (x, y) ∈ edgeSet (G₁ \ G₂) ↔ (x, y) ∈ edgeSet G₁ \ edgeSet G₂

State before:
case h.mk
ι : Sort ?u.55069
𝕜 : Type ?u.55072
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 y : V
⊢ (x, y) ∈ edgeSet (G₁ \ G₂) ↔ (x, y) ∈ edgeSet G₁ \ edgeSet G₂
Tactic:
rfl
State after:
no goals