Theorem: IMOSL.IMO2021A3.targetSum_general_lower_bound (IMOSLLean4/IMO2021/A3/A3.lean)

State before:
a : ℕ
l : List ℕ
⊢ (map Nat.succ (a :: l)).prod ≤ 2 ^ targetSum (a :: l) * (a :: l).length.factorial
Tactic:
rw [map_cons, prod_cons, targetSum, pow_add,
  length_cons, Nat.factorial_succ, mul_mul_mul_comm]
State after:
a : ℕ
l : List ℕ
⊢ a.succ * (map Nat.succ l).prod ≤ 2 ^ (a / l.length.succ) * (l.length + 1) * (2 ^ targetSum l * l.length.factorial)

State before:
a : ℕ
l : List ℕ
⊢ a.succ * (map Nat.succ l).prod ≤ 2 ^ (a / l.length.succ) * (l.length + 1) * (2 ^ targetSum l * l.length.factorial)
Tactic:
exact Nat.mul_le_mul (succ_le_mul_two_pow_div a l.length.succ_pos)
  (targetSum_general_lower_bound l)
State after:
no goals