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

State before:
l : List ℕ
n : ℕ
h : l ~ iota n
⊢ n.size ≤ targetSum l
Tactic:
have h0 := targetSum_general_lower_bound l
State after:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (map Nat.succ l).prod ≤ 2 ^ targetSum l * l.length.factorial
⊢ n.size ≤ targetSum l

State before:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (map Nat.succ l).prod ≤ 2 ^ targetSum l * l.length.factorial
⊢ n.size ≤ targetSum l
Tactic:
rw [(h.map Nat.succ).prod_eq, h.length_eq,
  prod_map_succ_iota, length_iota] at h0
State after:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (n + 1).factorial ≤ 2 ^ targetSum l * n.factorial
⊢ n.size ≤ targetSum l

State before:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (n + 1).factorial ≤ 2 ^ targetSum l * n.factorial
⊢ n.size ≤ targetSum l
Tactic:
exact Nat.size_le.mpr (Nat.le_of_mul_le_mul_right h0 n.factorial_pos)
State after:
no goals