obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf
ι : 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
⊢ 𝒜.card ≤ s.card.choose (s.card / 2)
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)
⊢ 𝒜.card ≤ s.card.choose (s.card / 2)