Erdos392.Params.initial_balance_eq

lemma Params.initial_balance_eq (P : Params) (p : ℕ) :    P.initial.balance p = (initial_full P).balance p -      (P.M : ℤ) * ∑ m ∈ rough_set P, (m.factorization p : ℤ) := by  unfold Factorization.balance rough_set  simp only [initial, initial_full]  unfold Factorization.sum  simp only [cast_multiset_sum, Multiset.map_map, Function.comp_apply, map_join, map_replicate,    sum_join, sum_map_val, sum_replicate, smul_eq_mul, cast_mul, cast_sum, sum_filter, ite_not]  induction P.M with  | zero => simp_all only [Nat.div_zero, tsub_zero, le_refl, Ico_eq_zero_of_le, replicate_zero,    join_zero, filter_zero, Multiset.map_zero, sum_zero, zero_sub, CharP.cast_eq_zero,    Ico_eq_empty_of_le, sum_empty, mul_zero]  | succ M ih =>    simp_all only [replicate_succ, join_cons, filter_add, Multiset.map_add, sum_add, cast_add,      cast_one, add_mul, one_mul]    rw [show (Multiset.filter (· ∈ (P.n / P.L).smoothNumbers)        (Multiset.replicate M (Multiset.Ico (P.n - P.n / (M + 1)) P.n)).join) =        Multiset.join (Multiset.replicate M (Multiset.filter (· ∈ (P.n / P.L).smoothNumbers)        (Multiset.Ico (P.n - P.n / (M + 1)) P.n))) from ?_]    · simp_all only [mul_sum, sum_ite, sum_const_zero, zero_add, sub_eq_iff_eq_add, map_join,      map_replicate, sum_join, sum_replicate, Int.nsmul_eq_mul]      simp only [add_comm, sub_eq_add_neg, filter_not, Finset.filter_subset, sum_sdiff_eq_sub,        add_assoc, neg_add_rev, neg_neg, add_left_comm, add_neg_cancel, zero_add,        add_neg_cancel_left]      rw [← Finset.mul_sum]      congr    · rw [Multiset.filter_join, Multiset.map_replicate]