no goals
ι : Sort ?u.132431
𝕜 : Type ?u.132434
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝³ : Fintype ↑(edgeSet G)
inst✝² : Fintype ↑(edgeSet G₁)
inst✝¹ : Fintype ↑(edgeSet G₂)
inst✝ : DecidableEq V
⊢ edgeFinset (G₁ \ G₂) = edgeFinset G₁ \ edgeFinset G₂
simp [edgeFinset]