case Adj.h.h.a
ι : Sort ?u.243913
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ SimpleGraph.Adj (SimpleGraph.deleteEdges (Subgraph.spanningCoe G') s) x✝¹ x✝ ↔
    SimpleGraph.Adj (Subgraph.spanningCoe (deleteEdges G' s)) x✝¹ x✝
ι : Sort ?u.243913
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ SimpleGraph.deleteEdges (Subgraph.spanningCoe G') s = Subgraph.spanningCoe (deleteEdges G' s)
ext
no goals
case Adj.h.h.a
ι : Sort ?u.243913
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ SimpleGraph.Adj (SimpleGraph.deleteEdges (Subgraph.spanningCoe G') s) x✝¹ x✝ ↔
    SimpleGraph.Adj (Subgraph.spanningCoe (deleteEdges G' s)) x✝¹ x✝
simp