Sum sum K i eq n sub d

lemma sum_sum_K_i_eq_n_sub_d (h_B : 2 ≤ B.card) :    ∑ i, sum_choose_K_i B i = choose_2 B.card * (n - d B) := by  have hd_eq_sum : 2 * choose_2 (B.card : ℚ) * d B =      n * 2 * choose_2 (B.card : ℚ) - 2 * ∑ i, ∑ α, choose_2 (K B i α) := by    have h_sum : ∑ i, ∑ x ∈ B ×ˢ B with x.1 ≠ x.2,        (if x.1 i ≠ x.2 i then 1 else 0) =        2 * choose_2 (B.card : ℚ) * n - 2 * ∑ i, ∑ α, choose_2 (K B i α) := by      have h_sum_rewrite :          ∑ i : Fin n, ∑ x ∈ B ×ˢ B with x.1 ≠ x.2,            (if x.1 i ≠ x.2 i then 1 else 0) =          ∑ i : Fin n,            (2 * choose_2 (B.card : ℚ) - 2 * ∑ α : F, choose_2 (K B i α)) :=        sum_congr rfl fun i _ ↦ sum_of_not_equals |>.trans (by ring)      rw [h_sum_rewrite, Finset.sum_sub_distrib, mul_sum _ _ _, sum_const,        Finset.card_fin, nsmul_eq_mul]; ring!    convert h_sum using 1 <;> ring_nf!    convert d_eq_sum h_B using 1; ring!  unfold choose_2 at *; norm_num at *; linarith!