Theorem: Finset.card_le_of_forall_dist_sum_le (LeanCamCombi/LittlewoodOfford.lean)

State before:
ι : 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)
Tactic:
obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf
State after:
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)

State before:
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)
Tactic:
rw [← hP]
State after:
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 ≤ P.parts.card

State before:
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
Tactic:
simpa only [exists_prop] using P.exists_mem (mem_powerset.2 $ h𝒜 _ ht)
State after:
no goals