case Adj.h.h.a
ι : Sort ?u.256926
V : Type u
W : Type v
G : SimpleGraph V
s : Set V
x✝¹ x✝ : ↑s
⊢ SimpleGraph.Adj (SimpleGraph.induce s G) x✝¹ x✝ ↔ SimpleGraph.Adj (Subgraph.coe (induce ⊤ s)) x✝¹ x✝
ι : Sort ?u.256926
V : Type u
W : Type v
G : SimpleGraph V
s : Set V
⊢ SimpleGraph.induce s G = Subgraph.coe (induce ⊤ s)
ext
no goals
case Adj.h.h.a
ι : Sort ?u.256926
V : Type u
W : Type v
G : SimpleGraph V
s : Set V
x✝¹ x✝ : ↑s
⊢ SimpleGraph.Adj (SimpleGraph.induce s G) x✝¹ x✝ ↔ SimpleGraph.Adj (Subgraph.coe (induce ⊤ s)) x✝¹ x✝
simp