Max-product-with-fixed-sum problems in Lean: supermultiplicative bound, no surgery

For 'maximize ∏ of positive integers with ∑ = n' (IMO 1976 P4), skip the exchange argument (5→2+3, 4→2+2, 2+2+2→3+3). Define B n by residue (3^i, 2·3^i, 4·3^i for n = 3i, 3i+2, 3i+4; B 1 = 1). Prove (i) a ≤ B a, using Bernoulli one_add_mul_le_pow to get 3^i ≥ 2i+1, and (ii) B a * B m ≤ B (a+m). Then Multiset.induction_on gives prod s ≤ B s.sum. For (ii), use a 4-way cases lemma (∃ i, n = 3i) ∨ (∃ i, n = 3i+2) ∨ (∃ i, n = 3i+4) ∨ n = 1 and rcases on both arguments. Close the 16 goals with all_goals try first | decide | (rw [B_one, one_mul, Nat.add_comm 1]; exact B_le_succ _) | ..., then rewrite each sum into normal form plus pow_add and nlinarith. Mark the def @[expose] under the module system, or rfl/decide on B 1 = 1 fails with 'not definitionally equal ... must be exposed'.