English
G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s for any G and s.
Русский
G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s для любых G и s.
LaTeX
$$$$ G.edgeSet \ (s \ {e \mid e.IsDiag}) = G.edgeSet \ s. $$$$
Lean4
/-- This lemma, combined with `edgeSet_sdiff` and `edgeSet_from_edgeSet`,
allows proving `(G \ from_edgeSet s).edge_set = G.edgeSet \ s` by `simp`. -/
@[simp]
theorem edgeSet_sdiff_sdiff_isDiag (G : SimpleGraph V) (s : Set (Sym2 V)) :
G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s := by
ext e
simp only [Set.mem_diff, Set.mem_setOf_eq, not_and, not_not, and_congr_right_iff]
intro h
simp only [G.not_isDiag_of_mem_edgeSet h, imp_false]