Erdos392.Params.initial.sum_valuation_eq

lemma Params.initial.sum_valuation_eq (P : Params) {p : ℕ} (hp : p.Prime)    (hp' : p > Real.sqrt P.n) (hps : p < P.n / P.L) : (P.initial.a.map (·.factorization p)).sum =    P.M * (Finset.filter (p ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card := by  have h1 : ∀ m ∈ Finset.Ico (P.n - P.n / P.M) P.n, (if m ∈ smoothNumbers (P.n / P.L)      then m.factorization p else 0) = if p ∣ m then 1 else 0 := fun m hm ↦ by    by_cases m = 0    · simp_all only [Finset.mem_Ico, nonpos_iff_eq_zero]      exact absurd hm.1        (Nat.ne_of_gt (Nat.sub_pos_of_lt          (Nat.div_lt_self hm.2 (by linarith [P.hM]))))    · simp_all [valuation_eq_indicator]  have h2 : (P.initial.a.map (·.factorization p)).sum =      P.M * ∑ m ∈ Finset.Ico (P.n - P.n / P.M) P.n,        if m ∈ smoothNumbers (P.n / P.L) then m.factorization p else 0 := by    have : (P.initial.a.map (·.factorization p)).sum =        (map (fun m ↦ if m ∈ smoothNumbers (P.n / P.L) then m.factorization p else 0)          (join (replicate P.M (Finset.Ico (P.n - P.n / P.M) P.n).val))).sum := by      conv_lhs => rw [show P.initial.a = filter (· ∈ smoothNumbers (P.n / P.L))          (join (replicate P.M (Finset.Ico (P.n - P.n / P.M) P.n).val)) from rfl]      induction (replicate P.M (Finset.Ico (P.n - P.n / P.M) P.n).val).join        using Multiset.induction <;> aesop    simp_all  simp_all [sum_congr rfl h1]