Theorem: SimpleGraph.deleteEdges_eq_self (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
s✝ s : Set (Sym2 α)
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s
Tactic:
rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]
State after:
no goals