Erdos392.Factorization.score_sum_change_multiset

lemma Factorization.score_sum_change_multiset {n : ℕ} (f f' : Factorization n) (L : ℕ)    (M : Multiset ℕ) (hM_le : M ≤ deficitMultiset f L)    (h_bal_eq : ∀ p ∈ (n + 1).primesBelow, f'.balance p = f.balance p + M.count p) :    (∑ q ∈ (n + 1).primesBelow,      if f'.balance q > 0 then (f'.balance q) * Real.log q      else if q ≤ L then (-f'.balance q) * Real.log L      else ↑(-f'.balance q) * Real.log (↑n / ↑q)) -    (∑ q ∈ (n + 1).primesBelow,      if f.balance q > 0 then ↑(f.balance q) * Real.log ↑q      else if q ≤ L then (-f.balance q) * Real.log ↑L      else ↑(-f.balance q) * Real.log (↑n / ↑q)) = -↑(M.card) * Real.log L := by  have h_term : ∀ p ∈ (n + 1).primesBelow,      (if f'.balance p > 0 then (f'.balance p : ℝ) * Real.log p       else if p ≤ L then (-f'.balance p : ℝ) * Real.log L       else (-f'.balance p : ℝ) * Real.log (n / p)) -      (if f.balance p > 0 then (f.balance p : ℝ) * Real.log p       else if p ≤ L then (-f.balance p : ℝ) * Real.log L       else (-f.balance p : ℝ) * Real.log (n / p)) = -M.count p * Real.log L := by    intro p hp    by_cases hdef : f.balance p < 0    · by_cases hL : p ≤ L <;> simp_all      · split_ifs <;> try linarith        have hcnt := Multiset.count_le_of_le p hM_le        rw [count_deficitMultiset] at hcnt        have : M.count p ≤ (f.balance p).natAbs := by grind        linarith [abs_of_neg hdef]      · have : M.count p = 0 := Nat.eq_zero_of_le_zero <|          (count_deficitMultiset f L p ▸ if_neg (by omega)).symm ▸            Multiset.count_le_of_le _ hM_le        aesop    · have : M.count p = 0 := Nat.eq_zero_of_le_zero <|        (count_deficitMultiset f L p ▸ if_neg (by tauto)).symm ▸          Multiset.count_le_of_le _ hM_le      aesop  have h_card : ∑ p ∈ (n + 1).primesBelow, M.count p = M.card := by    have aux : ∀ {S : Multiset ℕ}, (∀ p ∈ S, p ∈ (n + 1).primesBelow) →        ∑ p ∈ (n + 1).primesBelow, S.count p = S.card := by      intro S hS; induction S using Multiset.induction <;> aesop    refine aux fun p hp ↦ ?_    have hmem := Multiset.mem_of_le hM_le hp    simp only [deficitMultiset, filter_val, mem_bind, Multiset.mem_filter] at hmem ⊢    rcases hmem with ⟨a, ⟨ha, _⟩, hp⟩    exact (Multiset.mem_replicate.mp hp).2 ▸ ha  simp_all only [gt_iff_lt, Int.cast_add, Int.cast_natCast, neg_add_rev, neg_mul, Int.cast_neg,    ← sum_sub_distrib, sum_neg_distrib]  rw [← h_card, Nat.cast_sum, Finset.sum_mul]