simpa only [exists_prop] using P.exists_mem (mem_powerset.2 $ h𝒜 _ ht)
case intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
hr✝ : 0 < r
h𝒜 : ∀ t ∈ 𝒜, t ⊆ s
hf : ∀ i ∈ s, r ≤ ‖f i‖
h𝒜r : ∀ u ∈ 𝒜, ∀ v ∈ 𝒜, dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
_hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
t : Finset ι
ht : t ∈ 𝒜
⊢ ∃ b ∈ P.parts, (fun x x_1 => x ∈ x_1) t b
no goals