Card weigth Bound Indices eq sum

lemma card_weigthBoundIndices_eq_sum (D : ℕ) (hk : 1 < k) :    (weigthBoundIndices k D).card = ∑ j ∈ range (D / (k - 1) + 1), (D - (k - 1) * j + 1) := by    have h_split : (weigthBoundIndices k D).card =        ∑ j ∈ range (D / (k - 1) + 1),          ∑ i ∈ range (D + 1), if i + (k - 1) * j ≤ D then 1 else 0 := by      rw [show weigthBoundIndices k D =        filter (fun p : ℕ × ℕ ↦ p.1 + (k - 1) * p.2 ≤ D)        ((range (D + 1)).product (range (D / (k - 1) + 1))) from ?_, card_filter]      · erw [sum_product, Finset.sum_comm]      · ext ⟨i, j⟩        simp only [weigthBoundIndices, product_eq_sprod, mem_filter, mem_product, mem_range,          and_congr_left_iff, and_congr_right_iff]        exact fun _ _ ↦ iff_of_true (by          nlinarith [Nat.sub_pos_of_lt hk, D.div_add_mod (k - 1),            D.mod_lt (Nat.sub_pos_of_lt hk)])          (Nat.lt_succ_of_le (Nat.le_div_iff_mul_le (Nat.sub_pos_of_lt hk) |>.2          (by nlinarith [Nat.sub_pos_of_lt hk])))    have h_inner : ∀ j ∈ range (D / (k - 1) + 1), ∑ i ∈ range (D + 1),        (if i + (k - 1) * j ≤ D then 1 else 0) = (D - (k - 1) * j) + 1 := by      intro j hj      have h_filter : filter (fun i ↦ i + (k - 1) * j ≤ D) (range (D + 1)) =          Icc 0 (D - (k - 1) * j) := by        ext i        simp only [mem_filter, mem_range, mem_Icc, zero_le, true_and]        refine ⟨fun h ↦ Nat.le_sub_of_add_le <| by linarith, fun h ↦ ⟨by            nlinarith [Nat.sub_add_cancel <| show (k - 1) * j ≤ D from by              nlinarith [Nat.sub_add_cancel <| show j ≤ D / (k - 1) from by                linarith [mem_range.mp hj], Nat.div_mul_le_self D (k - 1)]], by                  linarith [Nat.sub_add_cancel <| show (k - 1) * j ≤ D from by                    nlinarith [Nat.sub_add_cancel <| show j ≤ D / (k - 1) from by                      linarith [mem_range.mp hj], Nat.div_mul_le_self D (k - 1)]]⟩⟩      simp_all    exact h_split.trans (sum_congr rfl h_inner)