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

State before:
ι : Sort ?u.54704
𝕜 : Type ?u.54707
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.54704
𝕜 : Type ?u.54707
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.54704
𝕜 : Type ?u.54707
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