Erdos392.Params.initial.sum_valuation_eq_small

lemma Params.initial.sum_valuation_eq_small (P : Params) {p : ℕ} (hp : p.Prime)    (hp_le : p ≤ Real.sqrt P.n) (hp_gt : p > P.L) :    (P.initial.a.map (·.factorization p)).sum =    P.M * ∑ k ∈ Finset.Ico 1 (Nat.log p P.n + 1),      (Finset.filter (p^k ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card := by  have h_sum_factorizations : (P.initial.a.map (·.factorization p)).sum =      P.M * (∑ m ∈ Finset.Ico (P.n - P.n / P.M) P.n, m.factorization p) := by    have h_sum_smooth : (P.initial.a.map (·.factorization p)).sum =        P.M * (∑ m ∈ filter (fun m ↦ m ∈ smoothNumbers (P.n / P.L))          (Ico (P.n - P.n / P.M) P.n), m.factorization p) := by      simp only [initial, join, sum_replicate, sum_filter, filter_nsmul]      simp only [Finset.sum_ite, sum_const_zero, add_zero]      induction P.M with      | zero => simp_all      | succ n ih =>        simp_all only [gt_iff_lt, add_smul, one_smul, Multiset.map_add, sum_add, succ_mul]        congr! 1        rw [Multiset.map_nsmul]        induction n with        | zero => simp_all        | succ n' ih' =>          simp_all only [Multiset.sum_nsmul, smul_eq_mul, succ_mul]          congr! 1    rw [h_sum_smooth, sum_filter_of_ne]    intro m hm hmp    specialize hmp    contrapose! hmp    simp_all +decide only [Finset.mem_Ico, factorization_eq_zero_iff, false_or]    refine Or.inl fun h ↦ hmp <| initial.smooth_of_dvd_small_prime P hp_le (by grind)      (Finset.mem_Ico.mpr ⟨by grind, by grind⟩) h  have h_sum_factorizations_eq : ∀ m ∈ Finset.Ico (P.n - P.n / P.M) P.n, m.factorization p =      ∑ k ∈ Ico 1 (Nat.log p P.n + 1), (if p ^ k ∣ m then 1 else 0) := by    intro m hm    have h_factorization_eq_sum : m.factorization p =        ∑ k ∈ Finset.Ico 1 (Nat.factorization m p + 1),        (if p ^ k ∣ m then 1 else 0) := by      simp_all only [sum_congr rfl fun x hx ↦ if_pos <| dvd_trans (pow_dvd_pow _ <|        Finset.mem_Ico.mp hx |>.2 |> Nat.lt_succ_iff.mp) <| ordProj_dvd .., succ_eq_add_one,          sum_const, card_Ico, add_tsub_cancel_right, smul_eq_mul, mul_one]    refine h_factorization_eq_sum.trans <| sum_subset ?_ ?_    · simp +contextual only [Finset.subset_iff, Finset.mem_Ico, true_and, and_imp]      refine fun k hk₁ hk₂ ↦ lt_succ_of_le (le_log_of_pow_le hp.one_lt ?_)      linarith [Finset.mem_Ico.mp hm, le_of_dvd (pos_of_ne_zero (by aesop_cat)) (ordProj_dvd m p),        Nat.pow_le_pow_right hp.one_lt.le (show k ≤ factorization m p from by grind)]    · simp +contextual only [Finset.mem_Ico, true_and, not_lt, ite_eq_right_iff, one_ne_zero,      imp_false, and_imp]      intro x hx₁ hx₂ hx₃      contrapose! hx₃      rw [← factorization_le_iff_dvd] at hx₃ <;> norm_num at *      · simpa [hp] using hx₃ p      · exact fun h ↦ absurd h hp.ne_zero      · rintro rfl        norm_num at *        exact hm.1.not_gt (div_lt_self hm.2 (by linarith [P.hM]))  rw [h_sum_factorizations, Finset.sum_congr rfl h_sum_factorizations_eq, Finset.sum_comm,    Finset.sum_congr rfl]  aesop