no goals
x : ℝ
⊢ cos (π / 2 ^ (0 + 1)) = sqrtTwoAddSeries 0 0 / 2
simp
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
x : ℝ
n : ℕ
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have : (2 : ℝ) ≠ 0 := two_ne_zero
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 (n + 1) / 2 = cos (π / 2 ^ (n + 1 + 1))
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
symm
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ cos (π / 2 ^ (n + 1 + 1)) * 2 = sqrtTwoAddSeries 0 (n + 1)
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 (n + 1) / 2 = cos (π / 2 ^ (n + 1 + 1))
rw [div_eq_iff_mul_eq this]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 (n + 1) = cos (π / 2 ^ (n + 1 + 1)) * 2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ cos (π / 2 ^ (n + 1 + 1)) * 2 = sqrtTwoAddSeries 0 (n + 1)
symm
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 / 2 * 2 ^ 2 + sqrtTwoAddSeries 0 n / 2 / 2 * 2 ^ 2 = 2 + sqrtTwoAddSeries 0 n

case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 (n + 1) = cos (π / 2 ^ (n + 1 + 1)) * 2
rw [sqrtTwoAddSeries, sqrt_eq_iff_sq_eq, mul_pow, cos_sq, ← mul_div_assoc, Nat.add_succ,
  pow_succ, mul_div_mul_left _ _ this, cos_pi_over_two_pow _, add_mul]
case e_a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 / 2 * 2 ^ 2 = 2

case e_a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 n / 2 / 2 * 2 ^ 2 = sqrtTwoAddSeries 0 n

case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 / 2 * 2 ^ 2 + sqrtTwoAddSeries 0 n / 2 / 2 * 2 ^ 2 = 2 + sqrtTwoAddSeries 0 n

case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
congr
case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
case e_a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ sqrtTwoAddSeries 0 n / 2 / 2 * 2 ^ 2 = sqrtTwoAddSeries 0 n

case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
rw [mul_comm, sq, mul_assoc, ← mul_div_assoc, mul_div_cancel_left, ← mul_div_assoc,
    mul_div_cancel_left] <;>
  try exact this
case hx.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2

case hx.hb
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
case hx
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
apply add_nonneg
case hx.hb
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
case hx.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ 2

case hx.hb
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
norm_num
case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
case hx.hb
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ sqrtTwoAddSeries 0 n

case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
apply sqrtTwoAddSeries_zero_nonneg
case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1))
case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1)) * 2
norm_num
case hy.a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < cos (π / 2 ^ (n + 1 + 1))
case hy
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 ≤ cos (π / 2 ^ (n + 1 + 1))
apply le_of_lt
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ -(π / 2) < π / 2 ^ (n + 1 + 1)

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ π / 2 ^ (n + 1 + 1) < π / 2
case hy.a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < cos (π / 2 ^ (n + 1 + 1))
apply cos_pos_of_mem_Ioo ⟨_, _⟩
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 < 2 ^ (n + 1 + 1)

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ π / 2 ^ (n + 1 + 1) < π / 2
apply div_lt_div' (le_refl π) _ pi_pos _
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ^ 1 < 2 ^ (n + 1 + 1)

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 < 2 ^ (n + 1 + 1)

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
refine' lt_of_le_of_lt (le_of_eq (pow_one _).symm) _
case h
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < 2

case h2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < n + 1 + 1

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ^ 1 < 2 ^ (n + 1 + 1)

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
apply pow_lt_pow
case h2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < n + 1 + 1

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
case h
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < 2

case h2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < n + 1 + 1

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
norm_num
case h2.a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < n + 1

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
case h2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 < n + 1 + 1

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
apply Nat.succ_lt_succ
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
case h2.a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < n + 1

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
apply Nat.succ_pos
no goals
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
all_goals norm_num
no goals
case e_a
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 1 / 2 * 2 ^ 2 = 2
norm_num
no goals
case e_a.ha
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 2 ≠ 0
exact this
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ -(π / 2) < 0

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2 ^ (n + 1 + 1)
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ -(π / 2) < π / 2 ^ (n + 1 + 1)
trans (0 : ℝ)
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2 ^ (n + 1 + 1)
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ -(π / 2) < 0

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2 ^ (n + 1 + 1)
rw [neg_lt_zero]
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2 ^ (n + 1 + 1)
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2

x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2 ^ (n + 1 + 1)
apply pi_div_two_pos
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2 ^ (n + 1 + 1)
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < π / 2 ^ (n + 1 + 1)
apply div_pos pi_pos
case H
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2 ^ (n + 1 + 1)
apply pow_pos
no goals
case H
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
norm_num
no goals
x : ℝ
n : ℕ
this : 2 ≠ 0
⊢ 0 < 2
norm_num