obtain ⟨g, hg, hgf⟩ :=
  exists_dual_vector ℝ (f i) (norm_pos_iff.1 $ hr.trans_le $ hf _ $ mem_insert_self _ _)
case insert.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)
⊢ ∃ 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‖
⊢ ∃ 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)