ext y
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
⊢ neighborFinset (G ⊓ H) x = neighborFinset G x ∩ neighborFinset H x
case a
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
y : V
⊢ y ∈ neighborFinset (G ⊓ H) x ↔ y ∈ neighborFinset G x ∩ neighborFinset H x