case h
ι : Sort ?u.223995
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v w : V
hvw : Adj G v w
hv : u ≠ v
hw : u ≠ w
x✝ : V
⊢ x✝ ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) u ↔ x✝ ∈ ∅
ι : Sort ?u.223995
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v w : V
hvw : Adj G v w
hv : u ≠ v
hw : u ≠ w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = ∅
ext
no goals
case h
ι : Sort ?u.223995
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v w : V
hvw : Adj G v w
hv : u ≠ v
hw : u ≠ w
x✝ : V
⊢ x✝ ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) u ↔ x✝ ∈ ∅
simp [hv.symm, hw.symm]