Theorem: SimpleGraph.neighborFinset_supr (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
inst✝² : DecidableEq V
ι : Type u_5
s : Finset ι
f : ι → SimpleGraph V
x : V
inst✝¹ : (i : ι) → Fintype ↑(neighborSet (f i) x)
inst✝ : Fintype ↑(neighborSet (sup s f) x)
⊢ neighborFinset (sup s f) x = Finset.biUnion s fun i => neighborFinset (f i) x
Tactic:
ext y
State after:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝² : DecidableEq V
ι : Type u_5
s : Finset ι
f : ι → SimpleGraph V
x : V
inst✝¹ : (i : ι) → Fintype ↑(neighborSet (f i) x)
inst✝ : Fintype ↑(neighborSet (sup s f) x)
y : V
⊢ y ∈ neighborFinset (sup s f) x ↔ y ∈ Finset.biUnion s fun i => neighborFinset (f i) x

State before:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝² : DecidableEq V
ι : Type u_5
s : Finset ι
f : ι → SimpleGraph V
x : V
inst✝¹ : (i : ι) → Fintype ↑(neighborSet (f i) x)
inst✝ : Fintype ↑(neighborSet (sup s f) x)
y : V
⊢ y ∈ neighborFinset (sup s f) x ↔ y ∈ Finset.biUnion s fun i => neighborFinset (f i) x
Tactic:
simp
State after:
no goals