case h
ι : Sort ?u.223079
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
⊢ u ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) v ↔ u ∈ {w}
ι : Sort ?u.223079
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) v = {w}
ext u
case h
ι : Sort ?u.223079
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
⊢ w = u ↔ u = w
case h
ι : Sort ?u.223079
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
⊢ u ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) v ↔ u ∈ {w}
suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this
no goals
case h
ι : Sort ?u.223079
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
⊢ w = u ↔ u = w
rw [eq_comm]
no goals
ι : Sort ?u.223079
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
this : w = u ↔ u = w
⊢ u ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) v ↔ u ∈ {w}
simpa [hvw.ne.symm] using this