Erdos392.Factorization.lower_score_3

@[blueprint  "score-lower-3"  (statement := /--  If there is a prime $p$ in deficit less than $L$, one can remove it without increasing the score.  -/)  (proof := /-- Without loss of generality we may assume that one is not in the previous two  situations, i.e., wlog there are no surplus primes and all primes in deficit are at most $L$.  If all deficit primes multiply to $n$ or less, add that product to the factorization (this  increases the waste by at most $\log n$, but we save a $\log n$ from now being in balance).  Otherwise, greedily multiply all primes together while staying below $n$ until one cannot do so  any further; add this product to the factorization, increasing the waste by at most $\log L$.-/)  (latexEnv := "sublemma")]theorem Factorization.lower_score_3 {n : ℕ} (f : Factorization n) (L : ℕ)    (hf : ∃ p ∈ (n + 1).primesBelow, p ≤ L ∧ f.balance p < 0) :    ∃ f' : Factorization n,      f'.total_imbalance < f.total_imbalance ∧ f'.score L ≤ f.score L := by  by_cases! h1 : ∃ p ∈ (n + 1).primesBelow, f.balance p > 0  · exact lower_score_1 f L h1  by_cases! h2 : ∃ p ∈ (n + 1).primesBelow, p > L ∧ f.balance p < 0  · exact lower_score_2 f L h2  refine lower_score_3_clean f L (fun p ↦ ?_) (fun p hp ↦ ?_) hf  · by_cases hp : p.Prime    · by_cases hp' : p ≤ n      · exact h1 p <| mem_primesBelow.mpr ⟨Nat.lt_succ_of_le hp', hp⟩      · have := fun m hm ↦ factorization_eq_zero_of_not_dvd fun h ↦ hp' <| (f.ha m hm).trans'          (le_of_dvd (f.hpos m hm) h); simp [balance, sum, map_congr rfl this]    · simp [balance, sum, factorization_eq_zero_of_not_prime _ hp]  · have hp_prime : p.Prime := of_not_not fun hnp ↦ hp.ne <| by simp [balance, sum,      factorization_eq_zero_of_not_prime _ hnp]    exact not_lt.mp fun hpL ↦ hp.not_ge <| h2 p (mem_primesBelow.mpr ⟨Nat.lt_succ_of_le      (deficit_implies_le_n f p hp), hp_prime⟩) hpL