Erdos392.Factorization.addFactor_submultiset_total_imbalance

lemma Factorization.addFactor_submultiset_total_imbalance {n : ℕ} (f : Factorization n) (L : ℕ)    (h_surplus : ∀ p, f.balance p ≤ 0) (M : Multiset ℕ) (hM : M ≤ deficitMultiset f L)    (m : ℕ) (hm : m ≤ n) (hm_pos : 0 < m) (h_m_prod : m = M.prod) :    (addFactor f m hm hm_pos).total_imbalance = f.total_imbalance - M.card := by  have h_bal : ∀ p ∈ (n + 1).primesBelow,      (addFactor f m hm hm_pos).balance p = f.balance p + M.count p := fun p _ ↦ by    rw [addFactor_balance, h_m_prod, factorization_prod_eq_count]    exact fun q hq ↦ (mem_deficitMultiset f L q (Multiset.mem_of_le hM hq)).1  have h_ptwise : ∀ p ∈ (n + 1).primesBelow,      (f.balance p + M.count p).natAbs = (f.balance p).natAbs - M.count p := fun p _ ↦ by    have h_count_le : M.count p ≤ (f.balance p).natAbs := by      have := Multiset.count_le_of_le p hM      rw [count_deficitMultiset] at this      aesop    have h_neg : f.balance p ≤ 0 := h_surplus p    have h1 : ((f.balance p).natAbs : ℤ) = -f.balance p := Int.ofNat_natAbs_of_nonpos h_neg    have h2 : ((f.balance p + M.count p).natAbs : ℤ) = -(f.balance p + M.count p) :=      Int.ofNat_natAbs_of_nonpos (by omega : f.balance p + M.count p ≤ 0)    omega  have h_sum : ∑ p ∈ (n + 1).primesBelow, (f.balance p + M.count p).natAbs =      ∑ p ∈ (n + 1).primesBelow, (f.balance p).natAbs -        ∑ p ∈ (n + 1).primesBelow, M.count p := by    have h_le : ∀ p ∈ (n + 1).primesBelow, M.count p ≤ (f.balance p).natAbs := fun p _ ↦ by      have := Multiset.count_le_of_le p hM      rw [count_deficitMultiset] at this      aesop    rw [Finset.sum_congr rfl h_ptwise]    have h_add : ∑ p ∈ (n + 1).primesBelow, ((f.balance p).natAbs - M.count p + M.count p) =        ∑ p ∈ (n + 1).primesBelow, (f.balance p).natAbs :=      Finset.sum_congr rfl fun x hx ↦ Nat.sub_add_cancel (h_le x hx)    rw [Finset.sum_add_distrib] at h_add    omega  have h_card_eq : ∀ {M : Multiset ℕ}, (∀ p ∈ M, p ∈ (n + 1).primesBelow) →      M.card = ∑ p ∈ (n + 1).primesBelow, M.count p := fun {M} hM ↦ by    induction M using Multiset.induction with    | empty => simp    | cons a M ih =>      simp only [Multiset.card_cons, Multiset.count_cons]      rw [ih (fun p hp ↦ hM p (Multiset.mem_cons_of_mem hp)), Finset.sum_add_distrib,          Finset.sum_ite_eq' _ a, if_pos (hM a (Multiset.mem_cons_self a M))]  convert! h_sum using 2  · simp only [total_imbalance]    exact Finset.sum_congr rfl fun p hp ↦ congrArg Int.natAbs (h_bal p hp)  · exact h_card_eq fun p hp ↦ by      obtain ⟨a, ha, ha'⟩ := Multiset.mem_bind.mp (Multiset.mem_of_le hM hp)      rw [Multiset.mem_replicate] at ha'      exact ha'.2 ▸ (Finset.mem_filter.mp ha).1