case h
ι : Sort ?u.148498
𝕜 : Type ?u.148501
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u✝ v✝ w✝ : V
e : Sym2 V
v w u : V
⊢ u ∈ commonNeighbors ⊤ v w ↔ u ∈ Set.univ \ {v, w}
ι : Sort ?u.148498
𝕜 : Type ?u.148501
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
v w : V
⊢ commonNeighbors ⊤ v w = Set.univ \ {v, w}
ext u
no goals
case h
ι : Sort ?u.148498
𝕜 : Type ?u.148501
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u✝ v✝ w✝ : V
e : Sym2 V
v w u : V
⊢ u ∈ commonNeighbors ⊤ v w ↔ u ∈ Set.univ \ {v, w}
simp [commonNeighbors, eq_comm, not_or]