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
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
apply lt_of_lt_of_le this (le_of_eq _)
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
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
rw [add_mul]
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)

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
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
congr 1
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
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
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]
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
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
apply pow_ne_zero
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 4 ≠ 0
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
norm_num
no goals
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 4 ≠ 0
norm_num
n : ℕ
⊢ π / 2 ^ (n + 2) < sin (π / 2 ^ (n + 2)) + 1 / (2 ^ n) ^ 3 / 4

n : ℕ
⊢ 0 < 2 ^ (n + 2)
n : ℕ
⊢ π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
rw [← div_lt_iff, ← sin_pi_over_two_pow_succ]
case refine'_1
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

case refine'_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ 1

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)
n : ℕ
⊢ π / 2 ^ (n + 2) < sin (π / 2 ^ (n + 2)) + 1 / (2 ^ n) ^ 3 / 4

n : ℕ
⊢ 0 < 2 ^ (n + 2)
refine' lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 / 4 ≤ 1 / (2 ^ n) ^ 3 / 4

n : ℕ
⊢ 0 < 2 ^ (n + 2)
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)
apply add_le_add_left
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)
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 / 4 ≤ 1 / (2 ^ n) ^ 3 / 4

n : ℕ
⊢ 0 < 2 ^ (n + 2)
rw [div_le_div_right]
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)
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)
rw [le_div_iff, ← mul_pow]
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)
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)
refine' le_trans _ (le_of_eq (one_pow 3))
case refine'_3.bc.ha
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2) * 2 ^ n

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)
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)
apply pow_le_pow_of_le_left
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)
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)
rw [← le_div_iff]
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)
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)
refine' le_trans ((div_le_div_right _).mpr pi_le_four) _
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)
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)
apply pow_pos
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)
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)
norm_num
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)
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)
rw [pow_succ, pow_succ, ← mul_assoc, ← div_div]
no goals
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)
all_goals (repeat' apply pow_pos); norm_num
case refine'_1
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case refine'_1
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
apply div_pos pi_pos
case refine'_1.H
n : ℕ
⊢ 0 < 2
case refine'_1
n : ℕ
⊢ 0 < 2 ^ (n + 2)
apply pow_pos
no goals
case refine'_1.H
n : ℕ
⊢ 0 < 2
norm_num
case refine'_2
n : ℕ
⊢ π ≤ 2 ^ (n + 2) * 1

case refine'_2
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case refine'_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ 1
rw [div_le_iff']
case refine'_2
n : ℕ
⊢ 4 ≤ 2 ^ (n + 2) * 1
case refine'_2
n : ℕ
⊢ π ≤ 2 ^ (n + 2) * 1
refine' le_trans pi_le_four _
case refine'_2
n : ℕ
⊢ 2 ^ 2 ≤ 2 ^ (n + 2)
case refine'_2
n : ℕ
⊢ 4 ≤ 2 ^ (n + 2) * 1
simp only [show (4 : ℝ) = (2 : ℝ) ^ 2 by norm_num, mul_one]
case refine'_2.ha
n : ℕ
⊢ 1 ≤ 2

case refine'_2.h
n : ℕ
⊢ 2 ≤ n + 2
case refine'_2
n : ℕ
⊢ 2 ^ 2 ≤ 2 ^ (n + 2)
apply pow_le_pow
case refine'_2.h
n : ℕ
⊢ 2 ≤ n + 2
case refine'_2.ha
n : ℕ
⊢ 1 ≤ 2

case refine'_2.h
n : ℕ
⊢ 2 ≤ n + 2
norm_num
case refine'_2.h.h
n : ℕ
⊢ 0 ≤ n
case refine'_2.h
n : ℕ
⊢ 2 ≤ n + 2
apply le_add_of_nonneg_left
no goals
case refine'_2.h.h
n : ℕ
⊢ 0 ≤ n
apply Nat.zero_le
no goals
n : ℕ
⊢ 4 = 2 ^ 2
norm_num
case refine'_2.H
n : ℕ
⊢ 0 < 2
case refine'_2
n : ℕ
⊢ 0 < 2 ^ (n + 2)
apply pow_pos
no goals
case refine'_2.H
n : ℕ
⊢ 0 < 2
norm_num
case refine'_3.bc.ha.a
n : ℕ
⊢ 0 < π / 2 ^ (n + 2) * 2 ^ n
case refine'_3.bc.ha
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2) * 2 ^ n
apply le_of_lt
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc.ha.a
n : ℕ
⊢ 0 < π / 2 ^ (n + 2) * 2 ^ n
apply mul_pos
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
apply div_pos pi_pos
case refine'_3.bc.ha.a.ha.H
n : ℕ
⊢ 0 < 2

case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
apply pow_pos
case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc.ha.a.ha.H
n : ℕ
⊢ 0 < 2

case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
norm_num
case refine'_3.bc.ha.a.hb.H
n : ℕ
⊢ 0 < 2
case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
apply pow_pos
no goals
case refine'_3.bc.ha.a.hb.H
n : ℕ
⊢ 0 < 2
norm_num
case H
n : ℕ
⊢ 0 < 2
n : ℕ
⊢ 0 < 2 ^ (n + 2)
(repeat' apply pow_pos)
no goals
case H
n : ℕ
⊢ 0 < 2
norm_num
case H
n : ℕ
⊢ 0 < 2
n : ℕ
⊢ 0 < 2 ^ (n + 2)
repeat' apply pow_pos
case H
n : ℕ
⊢ 0 < 2
case H
n : ℕ
⊢ 0 < 2
apply pow_pos
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ≠ 0
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)
rw [pow_succ _ (n + 1), ← mul_assoc, div_mul_cancel, mul_comm]
no goals
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ≠ 0
norm_num
no goals
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ 2 = 4
norm_num
no goals
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 * 2 = 4
norm_num