case Adj.h.mk.h.mk.a
ι : Sort ?u.246328
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s : Set (Sym2 V)
v : V
hv : v ∈ (deleteEdges G' s).verts
w : V
hw : w ∈ (deleteEdges G' s).verts
⊢ SimpleGraph.Adj (Subgraph.coe (deleteEdges G' s)) { val := v, property := hv } { val := w, property := hw } ↔
    SimpleGraph.Adj (SimpleGraph.deleteEdges (Subgraph.coe G') (Sym2.map Subtype.val ⁻¹' s))
      { val := v, property := hv } { val := w, property := hw }
ι : Sort ?u.246328
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s : Set (Sym2 V)
⊢ Subgraph.coe (deleteEdges G' s) = SimpleGraph.deleteEdges (Subgraph.coe G') (Sym2.map Subtype.val ⁻¹' s)
ext ⟨v, hv⟩ ⟨w, hw⟩
no goals
case Adj.h.mk.h.mk.a
ι : Sort ?u.246328
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s : Set (Sym2 V)
v : V
hv : v ∈ (deleteEdges G' s).verts
w : V
hw : w ∈ (deleteEdges G' s).verts
⊢ SimpleGraph.Adj (Subgraph.coe (deleteEdges G' s)) { val := v, property := hv } { val := w, property := hw } ↔
    SimpleGraph.Adj (SimpleGraph.deleteEdges (Subgraph.coe G') (Sym2.map Subtype.val ⁻¹' s))
      { val := v, property := hv } { val := w, property := hw }
simp