ι : Sort ?u.159422
𝕜 : Type ?u.159425
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
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.159422
𝕜 : Type ?u.159425
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
s s' : Set (Sym2 V)
h : s ⊆ s'
v w : V
⊢ Adj (deleteEdges G s') v w → Adj (deleteEdges G s) v w
simp (config := { contextual := true }) only [deleteEdges_adj, and_imp, true_and_iff]
no goals
ι : Sort ?u.159422
𝕜 : Type ?u.159425
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
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 _ hn hs => hn (h hs)