rw [delFedges_is_sdiff,_root_.sdiff_self]
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ delFedges G (edgeFinset G) ≤ H
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ ⊥ ≤ H