case a
ι : Sort ?u.282568
𝕜 : Type ?u.282571
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
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
a✝ : V
⊢ a✝ ∈ neighborFinset G v ↔ a✝ ∈ filter (Adj G v) univ
ι : Sort ?u.282568
𝕜 : Type ?u.282571
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
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
⊢ neighborFinset G v = filter (Adj G v) univ
ext
no goals
case a
ι : Sort ?u.282568
𝕜 : Type ?u.282571
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
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
a✝ : V
⊢ a✝ ∈ neighborFinset G v ↔ a✝ ∈ filter (Adj G v) univ
simp