[GOAL]
n : ℕ
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) < π
[PROOFSTEP]
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
[GOAL]
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
[PROOFSTEP]
rw [← lt_div_iff, ← sin_pi_over_two_pow_succ]
[GOAL]
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply sin_lt
[GOAL]
case h
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
all_goals apply pow_pos; norm_num
[GOAL]
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case h.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) < π
[PROOFSTEP]
apply lt_of_le_of_lt (le_of_eq _) this
[GOAL]
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)
[PROOFSTEP]
rw [pow_succ _ (n + 1), ← mul_assoc, div_mul_cancel, mul_comm]
[GOAL]
case h
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ π < 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
have : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / (2 : ℝ) + (1 : ℝ) / ((2 : ℝ) ^ n) ^ 3 / 4) * (2 : ℝ) ^ (n + 2) :=
  by
  rw [← div_lt_iff, ← sin_pi_over_two_pow_succ]
  refine' lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _
  · apply div_pos pi_pos; apply pow_pos; norm_num
  · rw [div_le_iff']
    · refine' le_trans pi_le_four _
      simp only [show (4 : ℝ) = (2 : ℝ) ^ 2 by norm_num, mul_one]
      apply pow_le_pow; norm_num; apply le_add_of_nonneg_left; apply Nat.zero_le
    · apply pow_pos; norm_num
  apply add_le_add_left; rw [div_le_div_right]
  rw [le_div_iff, ← mul_pow]
  refine' le_trans _ (le_of_eq (one_pow 3)); apply pow_le_pow_of_le_left
  · apply le_of_lt; apply mul_pos; apply div_pos pi_pos; apply pow_pos; norm_num; apply pow_pos
    norm_num
  rw [← le_div_iff]
  refine' le_trans ((div_le_div_right _).mpr pi_le_four) _; apply pow_pos; norm_num
  rw [pow_succ, pow_succ, ← mul_assoc, ← div_div]
    -- Porting note: removed `convert le_rfl`
  all_goals (repeat' apply pow_pos); norm_num
[GOAL]
n : ℕ
⊢ π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
[PROOFSTEP]
rw [← div_lt_iff, ← sin_pi_over_two_pow_succ]
[GOAL]
n : ℕ
⊢ π / 2 ^ (n + 2) < sin (π / 2 ^ (n + 2)) + 1 / (2 ^ n) ^ 3 / 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
refine' lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _
[GOAL]
case refine'_1
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
case refine'_1
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_1.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ 1
[PROOFSTEP]
rw [div_le_iff']
[GOAL]
case refine'_2
n : ℕ
⊢ π ≤ 2 ^ (n + 2) * 1
[PROOFSTEP]
refine' le_trans pi_le_four _
[GOAL]
case refine'_2
n : ℕ
⊢ 4 ≤ 2 ^ (n + 2) * 1
[PROOFSTEP]
simp only [show (4 : ℝ) = (2 : ℝ) ^ 2 by norm_num, mul_one]
[GOAL]
n : ℕ
⊢ 4 = 2 ^ 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
n : ℕ
⊢ 2 ^ 2 ≤ 2 ^ (n + 2)
[PROOFSTEP]
apply pow_le_pow
[GOAL]
case refine'_2.ha
n : ℕ
⊢ 1 ≤ 2
case refine'_2.h n : ℕ ⊢ 2 ≤ n + 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2.h
n : ℕ
⊢ 2 ≤ n + 2
[PROOFSTEP]
apply le_add_of_nonneg_left
[GOAL]
case refine'_2.h.h
n : ℕ
⊢ 0 ≤ n
[PROOFSTEP]
apply Nat.zero_le
[GOAL]
case refine'_2
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_2.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) + (π / 2 ^ (n + 2)) ^ 3 / 4 ≤ sin (π / 2 ^ (n + 2)) + 1 / (2 ^ n) ^ 3 / 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply add_le_add_left
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 / 4 ≤ 1 / (2 ^ n) ^ 3 / 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [div_le_div_right]
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 ≤ 1 / (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [le_div_iff, ← mul_pow]
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2) * 2 ^ n) ^ 3 ≤ 1
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
refine' le_trans _ (le_of_eq (one_pow 3))
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2) * 2 ^ n) ^ 3 ≤ 1 ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_le_pow_of_le_left
[GOAL]
case refine'_3.bc.ha
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2) * 2 ^ n
[PROOFSTEP]
apply le_of_lt
[GOAL]
case refine'_3.bc.ha.a
n : ℕ
⊢ 0 < π / 2 ^ (n + 2) * 2 ^ n
[PROOFSTEP]
apply mul_pos
[GOAL]
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
case refine'_3.bc.ha.a.hb n : ℕ ⊢ 0 < 2 ^ n
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case refine'_3.bc.ha.a.hb n : ℕ ⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.ha.a.ha.H
n : ℕ
⊢ 0 < 2
case refine'_3.bc.ha.a.hb n : ℕ ⊢ 0 < 2 ^ n
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.ha.a.hb.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ π / 2 ^ (n + 2) * 2 ^ n ≤ 1
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [← le_div_iff]
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
refine' le_trans ((div_le_div_right _).mpr pi_le_four) _
[GOAL]
case refine'_3.bc.hab.refine'_1
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.refine'_1.H
n : ℕ
⊢ 0 < 2
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [pow_succ, pow_succ, ← mul_assoc, ← div_div]
  -- Porting note: removed `convert le_rfl`
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
all_goals (repeat' apply pow_pos); norm_num
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.H
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.H.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.H.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < 4
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < 4
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply pow_pos
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ π < 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
apply lt_of_lt_of_le this (le_of_eq _)
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) =
    2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
rw [add_mul]
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) + 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) =
    2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) = 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n)
[PROOFSTEP]
rw [pow_succ _ (n + 1), ← mul_assoc, div_mul_cancel, mul_comm]
[GOAL]
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case e_a
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) = 1 / 4 ^ n
[PROOFSTEP]
rw [pow_succ, ← pow_mul, mul_comm n 2, pow_mul, show (2 : ℝ) ^ 2 = 4 by norm_num, pow_succ, pow_succ, ←
  mul_assoc (2 : ℝ), show (2 : ℝ) * 2 = 4 by norm_num, ← mul_assoc, div_mul_cancel, mul_comm ((2 : ℝ) ^ n), ← div_div,
  div_mul_cancel]
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ 2 = 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 * 2 = 4
[PROOFSTEP]
norm_num
[GOAL]
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ n ≠ 0
case e_a.h n : ℕ this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) ⊢ 4 ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case e_a.h.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ≠ 0
case e_a.h n : ℕ this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) ⊢ 4 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 4 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a < π
[PROOFSTEP]
refine' lt_of_le_of_lt _ (pi_gt_sqrtTwoAddSeries n)
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ sqrt (2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)
[PROOFSTEP]
refine' (div_le_iff (pow_pos (by norm_num) _ : (0 : ℝ) < _)).mp (le_sqrt_of_sq_le _)
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ (a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n
[PROOFSTEP]
rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 = ↑0 / ↑1
[PROOFSTEP]
rw [Nat.cast_zero, zero_div]
[GOAL]
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrtTwoAddSeries (↑a / ↑b) (n + 1) ≤ z
[PROOFSTEP]
refine' le_trans _ hz
[GOAL]
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrtTwoAddSeries (↑a / ↑b) (n + 1) ≤ sqrtTwoAddSeries (↑c / ↑d) n
[PROOFSTEP]
rw [sqrtTwoAddSeries_succ]
[GOAL]
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrtTwoAddSeries (sqrt (2 + ↑a / ↑b)) n ≤ sqrtTwoAddSeries (↑c / ↑d) n
[PROOFSTEP]
apply sqrtTwoAddSeries_monotone_left
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
[PROOFSTEP]
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
[PROOFSTEP]
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
[PROOFSTEP]
rw [sqrt_le_left (div_nonneg c.cast_nonneg d.cast_nonneg), div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hb'),
  div_le_div_iff hb' (pow_pos hd' _)]
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b
[PROOFSTEP]
exact_mod_cast h
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ π < a
[PROOFSTEP]
refine' lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) _
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n ≤ a
[PROOFSTEP]
rw [← le_sub_iff_add_le, ← le_div_iff', sqrt_le_left, sub_le_comm]
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n
[PROOFSTEP]
rwa [Nat.cast_zero, zero_div] at h 
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)
[PROOFSTEP]
exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)
[PROOFSTEP]
exact pow_pos zero_lt_two _
[GOAL]
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ z ≤ sqrtTwoAddSeries (↑c / ↑d) (n + 1)
[PROOFSTEP]
apply le_trans hz
[GOAL]
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ sqrtTwoAddSeries (↑a / ↑b) n ≤ sqrtTwoAddSeries (↑c / ↑d) (n + 1)
[PROOFSTEP]
rw [sqrtTwoAddSeries_succ]
[GOAL]
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ sqrtTwoAddSeries (↑a / ↑b) n ≤ sqrtTwoAddSeries (sqrt (2 + ↑c / ↑d)) n
[PROOFSTEP]
apply sqrtTwoAddSeries_monotone_left
[GOAL]
case h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ ↑a / ↑b ≤ sqrt (2 + ↑c / ↑d)
[PROOFSTEP]
apply le_sqrt_of_sq_le
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
[PROOFSTEP]
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
[PROOFSTEP]
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
[PROOFSTEP]
rw [div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hd'), div_le_div_iff (pow_pos hb' _) hd']
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ ↑a ^ 2 * ↑d ≤ (2 * ↑d + ↑c) * ↑b ^ 2
[PROOFSTEP]
exact_mod_cast h
[GOAL]
⊢ 3 < π
[PROOFSTEP]
pi_lower_bound [23 / 16]
[GOAL]
⊢ 3.14 < π
[PROOFSTEP]
pi_lower_bound [99 / 70, 874 / 473, 1940 / 989, 1447 / 727]
[GOAL]
⊢ π < 3.15
[PROOFSTEP]
pi_upper_bound [140 / 99, 279 / 151, 51 / 26, 412 / 207]
[GOAL]
⊢ 3.1415 < π
[PROOFSTEP]
pi_lower_bound [11482 / 8119, 5401 / 2923, 2348 / 1197, 11367 / 5711, 25705 / 12868, 23235 / 11621]
[GOAL]
⊢ π < 3.1416
[PROOFSTEP]
pi_upper_bound [4756 / 3363, 101211 / 54775, 505534 / 257719, 83289 / 41846, 411278 / 205887, 438142 / 219137,
  451504 / 225769, 265603 / 132804, 849938 / 424971]
[GOAL]
⊢ 3.141592 < π
[PROOFSTEP]
pi_lower_bound [11482 / 8119, 7792 / 4217, 54055 / 27557, 949247 / 476920, 3310126 / 1657059, 2635492 / 1318143,
  1580265 / 790192, 1221775 / 610899, 3612247 / 1806132, 849943 / 424972]
[GOAL]
⊢ π < 3.141593
[PROOFSTEP]
pi_upper_bound [27720 / 19601, 56935 / 30813, 49359 / 25163, 258754 / 130003, 113599 / 56868, 1101994 / 551163,
  8671537 / 4336095, 3877807 / 1938940, 52483813 / 26242030, 56946167 / 28473117, 23798415 / 11899211]
