x : ℝ
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 = sin (π / 2 ^ (n + 2))
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) = sqrt (2 - sqrtTwoAddSeries 0 n) / 2
symm
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) * 2 = sqrt (2 - sqrtTwoAddSeries 0 n)

x : ℝ
n : ℕ
⊢ 2 ≠ 0
x : ℝ
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 = sin (π / 2 ^ (n + 2))
rw [div_eq_iff_mul_eq]
x : ℝ
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) = sin (π / 2 ^ (n + 2)) * 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) * 2 = sqrt (2 - sqrtTwoAddSeries 0 n)

x : ℝ
n : ℕ
⊢ 2 ≠ 0
symm
x : ℝ
n : ℕ
⊢ 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2 = 2 - sqrtTwoAddSeries 0 n

case hx
x : ℝ
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
x : ℝ
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) = sin (π / 2 ^ (n + 2)) * 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
rw [sqrt_eq_iff_sq_eq, mul_pow, sin_sq_pi_over_two_pow_succ, sub_mul]
case hy.a
x : ℝ
n : ℕ
⊢ 0 < sin (π / 2 ^ (n + 2)) * 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy
x : ℝ
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
apply le_of_lt
case hy.a.ha
x : ℝ
n : ℕ
⊢ 0 < sin (π / 2 ^ (n + 2))

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a
x : ℝ
n : ℕ
⊢ 0 < sin (π / 2 ^ (n + 2)) * 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
apply mul_pos
case hy.a.ha.h0x
x : ℝ
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ π / 2 ^ (n + 2) < π

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha
x : ℝ
n : ℕ
⊢ 0 < sin (π / 2 ^ (n + 2))

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
apply sin_pos_of_pos_of_lt_pi
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ π / 2 ^ (n + 2) < π / 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ π / 2 ^ (n + 2) < π

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
refine' lt_of_lt_of_le _ (le_of_eq (div_one _))
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ 1 < 2 ^ (n + 2)

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ π / 2 ^ (n + 2) < π / 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
rw [div_lt_div_left]
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ 2 ^ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ 1 < 2 ^ (n + 2)

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
refine' lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _
case hy.a.ha.hxp.h
x : ℝ
n : ℕ
⊢ 1 < 2

case hy.a.ha.hxp.h2
x : ℝ
n : ℕ
⊢ 0 < n + 2

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp
x : ℝ
n : ℕ
⊢ 2 ^ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
apply pow_lt_pow
case hy.a.ha.hxp.h2
x : ℝ
n : ℕ
⊢ 0 < n + 2

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp.h
x : ℝ
n : ℕ
⊢ 1 < 2

case hy.a.ha.hxp.h2
x : ℝ
n : ℕ
⊢ 0 < n + 2

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
norm_num
case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp.h2
x : ℝ
n : ℕ
⊢ 0 < n + 2

case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
apply Nat.succ_pos
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp.ha
x : ℝ
n : ℕ
⊢ 0 < π

case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
apply pi_pos
case hy.a.ha.hxp.hb.H
x : ℝ
n : ℕ
⊢ 0 < 2

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
case hy.a.ha.hxp.hb
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
apply pow_pos
no goals
case hy.a.ha.hxp.hb.H
x : ℝ
n : ℕ
⊢ 0 < 2

case hy.a.ha.hxp.hc
x : ℝ
n : ℕ
⊢ 0 < 1

case hy.a.hb
x : ℝ
n : ℕ
⊢ 0 < 2

x : ℝ
n : ℕ
⊢ 2 ≠ 0
all_goals norm_num
no goals
x : ℝ
n : ℕ
⊢ 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2 = 2 - sqrtTwoAddSeries 0 n
congr <;> norm_num
case hx
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2
case hx
x : ℝ
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n
rw [sub_nonneg]
case hx.a
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2
case hx
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2
apply le_of_lt
no goals
case hx.a
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2
apply sqrtTwoAddSeries_lt_two
case hy.a.ha.h0x
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case hy.a.ha.h0x
x : ℝ
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
apply div_pos pi_pos
case hy.a.ha.h0x.H
x : ℝ
n : ℕ
⊢ 0 < 2
case hy.a.ha.h0x
x : ℝ
n : ℕ
⊢ 0 < 2 ^ (n + 2)
apply pow_pos
no goals
case hy.a.ha.h0x.H
x : ℝ
n : ℕ
⊢ 0 < 2
norm_num
no goals
x : ℝ
n : ℕ
⊢ 2 ≠ 0
norm_num