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

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