n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) < π
n : ℕ
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) < π
have : sqrt (2 - sqrtTwoAddSeries 0 n) / (2 : ℝ) * (2 : ℝ) ^ (n + 2) < π := by
  rw [← lt_div_iff, ← sin_pi_over_two_pow_succ]; apply sin_lt; apply div_pos pi_pos
  all_goals apply pow_pos; norm_num
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) = sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2)
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) < π
apply lt_of_le_of_lt (le_of_eq _) this
case h
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ≠ 0
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) = sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2)
rw [pow_succ _ (n + 1), ← mul_assoc, div_mul_cancel, mul_comm]
no goals
case h
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ≠ 0
norm_num
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
rw [← lt_div_iff, ← sin_pi_over_two_pow_succ]
case h
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)
apply sin_lt
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)
case h
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)
apply div_pos pi_pos
no goals
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)
all_goals apply pow_pos; norm_num
case H
n : ℕ
⊢ 0 < 2
n : ℕ
⊢ 0 < 2 ^ (n + 2)
apply pow_pos
no goals
case H
n : ℕ
⊢ 0 < 2
norm_num