Theorem: SimpleGraph.neighborSet_iSup (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
s : ι → SimpleGraph V
x : V
⊢ neighborSet (⨆ i, s i) x = ⋃ i, neighborSet (s i) x
Tactic:
ext y
State after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨆ i, s i) x ↔ y ∈ ⋃ i, neighborSet (s i) x

State before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨆ i, s i) x ↔ y ∈ ⋃ i, neighborSet (s i) x
Tactic:
simp
State after:
no goals