Erdos392.Factorization.lower_score_3_case2b

lemma Factorization.lower_score_3_case2b {n : ℕ} (f : Factorization n) (L : ℕ)    (h_surplus : ∀ p, f.balance p ≤ 0)    (hf : ∃ p ∈ (n + 1).primesBelow, p ≤ L ∧ f.balance p < 0)    (h_prod : n < (deficitMultiset f L).prod)    (hL_le_n : L ≤ n) :    ∃ f' : Factorization n,      f'.total_imbalance < f.total_imbalance ∧ f'.score L ≤ f.score L := by  obtain ⟨p₀, hp₀_mem, hp₀_le, hp₀_bal⟩ := hf  have hp₀ := prime_of_mem_primesBelow hp₀_mem  obtain ⟨M, hM_sub, hM_lb, hM_ub⟩ := exists_submultiset_prod_between (deficitMultiset f L)    (hp₀.pos.trans_le hp₀_le) ((hp₀.pos.trans_le hp₀_le).trans_le hL_le_n)      (fun p hp ↦ (mem_deficitMultiset f L p hp).2) h_prod  refine ⟨addFactor f M.prod hM_ub (pos_of_ne_zero fun h ↦ by grind), ?_, ?_⟩  · have h_imb := addFactor_submultiset_total_imbalance f L h_surplus M hM_sub      M.prod hM_ub (pos_of_ne_zero fun h ↦ by grind) rfl    refine h_imb ▸ sub_lt ?_ <| card_pos.mpr (by grind)    exact pos_of_ne_zero fun h ↦      hp₀_bal.ne <| by        have := sum_eq_zero_iff.mp h _ hp₀_mem        grind  · exact score_le_of_add_submultiset f L M hM_sub M.prod hM_ub (by grind) rfl hM_lb      (card_pos.mpr (by grind)) <| hp₀.two_le.trans hp₀_le