Theorem: IMOSL.IMO2013N2.final_solution (IMOSLLean4/IMO2013/N2/N2.lean)

State before:
n : ℕ
h : 0 < n
⊢ ↑(n + (2 ^ 0 - 1)) / ↑n = (map (fun m => ↑(m + 1) / ↑m) 0).prod
Tactic:
rw [pow_zero, Nat.sub_self, add_zero]
State after:
n : ℕ
h : 0 < n
⊢ ↑n / ↑n = (map (fun m => ↑(m + 1) / ↑m) 0).prod

State before:
n : ℕ
h : 0 < n
⊢ ↑n / ↑n = (map (fun m => ↑(m + 1) / ↑m) 0).prod
Tactic:
exact div_self (Nat.cast_ne_zero.mpr h.ne.symm)
State after:
no goals

State before:
k : ℕ
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Tactic:
have h := good_two_mul_add_one (final_solution k)
State after:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
⊢ good (k + 1) (2 ^ (k + 1) - 1)

State before:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Tactic:
have h0 := k.one_le_pow 2 (Nat.succ_pos 1)
State after:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
h0 : 1 ≤ 2 ^ k
⊢ good (k + 1) (2 ^ (k + 1) - 1)

State before:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
h0 : 1 ≤ 2 ^ k
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Tactic:
rwa [two_mul, add_assoc, Nat.sub_add_cancel h0, add_comm _ (2 ^ k),
  ← Nat.add_sub_assoc h0, ← two_mul, ← pow_succ'] at h
State after:
no goals