no goals
ι : Sort ?u.261642
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v : V
⊢ SimpleGraph.singletonSubgraph G v = induce ⊤ {v}
ext <;> simp (config := { contextual := true }) [-Set.bot_eq_empty, Prop.bot_eq_false]