case Adj.h.h.a
ι : Sort ?u.154730
𝕜 : Type ?u.154733
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 : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges G s) x✝¹ x✝ ↔ Adj (G \ fromEdgeSet s) x✝¹ x✝
ι : Sort ?u.154730
𝕜 : Type ?u.154733
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 : Set (Sym2 V)
⊢ deleteEdges G s = G \ fromEdgeSet s
ext
no goals
case Adj.h.h.a
ι : Sort ?u.154730
𝕜 : Type ?u.154733
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 : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges G s) x✝¹ x✝ ↔ Adj (G \ fromEdgeSet s) x✝¹ x✝
exact ⟨fun h => ⟨h.1, not_and_of_not_left _ h.2⟩, fun h => ⟨h.1, not_and'.mp h.2 h.ne⟩⟩