no goals
ι : Sort ?u.224643
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
u v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
split_ifs <;> subst_vars <;> simp [*]