choose t ht using fun 𝒜 (h𝒜 : 𝒜 ∈ P.parts) ↦
  Finset.exists_max_image _ (fun t ↦ g (∑ i in t, f i)) (P.nonempty_of_mem_parts h𝒜)
case insert.intro.intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
g : E →L[ℝ] ℝ
hg : ‖g‖ = 1
hgf : g (f i) = ↑‖f i‖
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
case insert.intro.intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
g : E →L[ℝ] ℝ
hg : ‖g‖ = 1
hgf : g (f i) = ↑‖f i‖
t : (𝒜 : Finset (Finset ι)) → 𝒜 ∈ P.parts → Finset ι
ht : ∀ (𝒜 : Finset (Finset ι)) (h𝒜 : 𝒜 ∈ P.parts), t 𝒜 h𝒜 ∈ 𝒜 ∧ ∀ x' ∈ 𝒜, g (∑ i ∈ x', f i) ≤ g (∑ i ∈ t 𝒜 h𝒜, f i)
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)