Sum choose K

lemma sum_choose_K' [Zero F] (h_card : 2 ≤ card F) :    (card F - 1) * choose_2 ((B.card - K B i 0) / (card F - 1)) ≤    ∑ α with α ≠ 0, choose_2 (K B i α) := by  rw [← sum_K_eq_card (i := i), Nat.cast_sum]  set x1 : ℚ := card F - 1  have hx1 : x1 ≠ 0 := by simp [x1, sub_eq_zero]; omega  set x2 := K B i  suffices x1 * choose_2      (∑ x with x ≠ 0, (fun _ ↦ x1⁻¹) x • (Nat.cast (R := ℚ) ∘ x2) x) ≤      ∑ α with α ≠ 0, choose_2 ↑(x2 α) by    simp only [ne_eq, Function.comp_apply, smul_eq_mul] at this; convert this    rw [sum_eq_sum_sdiff_singleton_add (i := 0) (by simp)]    ring_nf; rw [sum_mul]    apply Finset.sum_congr (ext _)    all_goals grind only [= mem_filter, = mem_sdiff, ← mem_univ, = mem_singleton]  simp only [Function.comp_apply, smul_eq_mul]  have hx1_nonneg : (0 : ℚ) ≤ x1 := by simp [x1, sub_nonneg]; omega  have jensen := ConvexOn.map_sum_le choose_2_convex    (t := univ.filter (· ≠ (0 : F))) (w := fun _ ↦ x1⁻¹) (p := fun α ↦ (x2 α : ℚ))    (fun _ _ ↦ inv_nonneg.mpr hx1_nonneg)    (by simp [x1]; field_simp; exact div_self hx1) (by simp)  simp only [smul_eq_mul] at jensen  exact le_trans (mul_le_mul_of_nonneg_left jensen hx1_nonneg) <|    le_of_eq <| by rw [mul_sum]; congr 1; ext; rw [← mul_assoc, mul_inv_cancel₀ hx1, one_mul]