ι : Sort ?u.223778
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G (_ : Adj G w v)) w = {v}
ι : Sort ?u.223778
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) w = {v}
rw [subgraphOfAdj_symm hvw.symm]
no goals
ι : Sort ?u.223778
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G (_ : Adj G w v)) w = {v}
exact neighborSet_fst_subgraphOfAdj hvw.symm