Erdos392.Factorization.zero_total_imbalance

@[blueprint  "balance-zero"  (statement := /-- If a factorization has zero total imbalance, then it exactly factors $n!$.-/)  (latexEnv := "lemma")]theorem Factorization.zero_total_imbalance {n : ℕ} (f : Factorization n)    (hf : f.total_imbalance = 0) : f.prod id = n.factorial := by  have h_balance_zero : ∀ p ∈ (n + 1).primesBelow, f.balance p = 0 := fun p hp ↦ by    have := Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ Nat.zero_le _) |>.mp hf p hp    omega  have h0 : (0 : ℕ) ∉ f.a := fun h ↦ (f.hpos 0 h).false  simp only [prod, Multiset.map_id]  refine eq_of_factorization_eq (Multiset.prod_ne_zero h0) (factorial_pos n).ne' fun p ↦ ?_  by_cases hp : p.Prime <;> by_cases hp_le : p ≤ n  · have hbal := h_balance_zero p (mem_primesBelow.mpr ⟨lt_succ_of_le hp_le, hp⟩)    unfold balance sum at hbal    simp only [factorization_multiset_prod f.a h0]    omega  · simp only [factorization_multiset_prod f.a h0,      factorization_factorial_eq_zero_of_lt (lt_of_not_ge hp_le)]    exact Multiset.sum_eq_zero fun x hx ↦ by      obtain ⟨m, hm, rfl⟩ := Multiset.mem_map.mp hx      exact factorization_eq_zero_of_lt ((f.ha m hm).trans_lt (lt_of_not_ge hp_le))  · aesop  · aesop