Erdos392.Factorization.lower_score_1

@[blueprint  "score-lower-1"  (statement := /-- If there is a prime $p$ in surplus, one can remove it without increasing the  score. -/)  (proof := /-- Locate a factor $a_i$ that contains the surplus prime $p$, then  replace $a_i$ with $a_i/p$.-/)  (latexEnv := "sublemma")]theorem Factorization.lower_score_1 {n : ℕ} (f : Factorization n) (L : ℕ)    (hf : ∃ p ∈ (n + 1).primesBelow, f.balance p > 0) :    ∃ f' : Factorization n,      f'.total_imbalance < f.total_imbalance ∧ f'.score L ≤ f.score L := by  obtain ⟨p, hp_mem, hp_pos⟩ := hf  obtain ⟨m, hm, h_fac_pos⟩ : ∃ m ∈ f.a, 0 < m.factorization p := by    contrapose! hp_pos    simp_all [balance, sum]  exact ⟨_, replace_div_total_imbalance f m p hm h_fac_pos (prime_of_mem_primesBelow hp_mem)    hp_mem hp_pos, replace_div_score_le f m p hm h_fac_pos (prime_of_mem_primesBelow hp_mem)      hp_mem hp_pos L⟩