case right
ι : Sort ?u.250888
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, Adj G' v w → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s' → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s
ι : Sort ?u.250888
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ deleteEdges G' s' ≤ deleteEdges G' s
constructor <;> simp (config := { contextual := true }) only [deleteEdges_verts, deleteEdges_adj,
  true_and_iff, and_imp, subset_rfl]
no goals
case right
ι : Sort ?u.250888
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, Adj G' v w → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s' → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s
exact fun _ _ _ hs' hs ↦ hs' (h hs)