-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_lt_sqrtTwoAddSeries (n : ℕ) :
    π < 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Proof state:
n : ℕ
⊢ 0 ≤ 2 ^ (n + 2)

Tactic:
positivity

Result:
no goals

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

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
⊢ π < 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Tactic:
have : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * (2 : ℝ) ^ (n + 2) := by
  rw [← div_lt_iff₀ (by norm_num), ← sin_pi_over_two_pow_succ, ← sub_lt_iff_lt_add']
  calc
    π / 2 ^ (n + 2) - sin (π / 2 ^ (n + 2)) < (π / 2 ^ (n + 2)) ^ 3 / 4 :=
      sub_lt_comm.1 <| sin_gt_sub_cube (by positivity) <| div_le_one_of_le₀ ?_ (by positivity)
    _ ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4 := by gcongr; exact pi_le_four
    _ = 1 / (2 ^ n) ^ 3 / 4 := by simp [add_comm n, pow_add, div_mul_eq_div_div]; norm_num
  calc
    π ≤ 4 := pi_le_four
    _ = 2 ^ (0 + 2) := by norm_num
    _ ≤ 2 ^ (n + 2) := by gcongr <;> norm_num

Result:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ π < 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Proof state:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Tactic:
rw [add_mul]

Result:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) + 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Proof state:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) + 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Tactic:
congr 1

Result:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) = 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) = 1 / 4 ^ n

Proof state:
n : ℕ
⊢ (4 / 2 ^ (n + 2)) ^ 3 / 4 = 1 / (2 ^ n) ^ 3 / 4

Tactic:
simp [add_comm n, pow_add, div_mul_eq_div_div]

Result:
n : ℕ
⊢ (4 / 2 ^ 2 / 2 ^ n) ^ 3 / 4 = ((2 ^ n) ^ 3)⁻¹ / 4

Proof state:
n : ℕ
⊢ π ≤ 2 ^ (n + 2)

Tactic:
calc
  π ≤ 4 := pi_le_four
  _ = 2 ^ (0 + 2) := by norm_num
  _ ≤ 2 ^ (n + 2) := by gcongr <;> norm_num

Result:
no goals

Proof state:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / 2 ^ (n * 3 + 2) * 2 ^ (n + 2) = 1 / 2 ^ (2 * n)

Tactic:
rw [one_div, one_div, inv_mul_eq_iff_eq_mul₀, eq_comm, mul_inv_eq_iff_eq_mul₀, ← pow_add]

Result:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) = 2 ^ (n + 2 + 2 * n)

case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (2 * n) ≠ 0

case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) ≠ 0

Proof state:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ π < 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Tactic:
refine lt_of_lt_of_le this (le_of_eq ?_)

Result:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) =
    2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

Proof state:
n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 / 4 ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4

Tactic:
gcongr

Result:
case hab.hab.hab
n : ℕ
⊢ π ≤ 4

Proof state:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)

Tactic:
rw [← div_lt_iff₀ (by norm_num), ← sin_pi_over_two_pow_succ, ← sub_lt_iff_lt_add']

Result:
n : ℕ
⊢ π / 2 ^ (n + 2) - sin (π / 2 ^ (n + 2)) < 1 / (2 ^ n) ^ 3 / 4

Proof state:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (2 * n) ≠ 0

case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) ≠ 0

Tactic:
all_goals norm_num

Result:
no goals

Proof state:
case hab.hab.hab
n : ℕ
⊢ π ≤ 4

Tactic:
exact pi_le_four

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < 2 ^ (n + 2)

Tactic:
norm_num

Result:
no goals

Proof state:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (n * 3 + 2) = 2 ^ (n + 2 + 2 * n)

Tactic:
rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n]

Result:
no goals

Proof state:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) = 1 / 4 ^ n

Tactic:
simp only [show (4 : ℝ) = 2 ^ 2 by norm_num, ← pow_mul, div_div, ← pow_add]

Result:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / 2 ^ (n * 3 + 2) * 2 ^ (n + 2) = 1 / 2 ^ (2 * n)

Proof state:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) = 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ 2 ^ (0 + 2) ≤ 2 ^ (n + 2)

Tactic:
gcongr <;> norm_num

Result:
no goals

Proof state:
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 4 = 2 ^ 2

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ π / 2 ^ (n + 2) - sin (π / 2 ^ (n + 2)) < 1 / (2 ^ n) ^ 3 / 4

Tactic:
calc
  π / 2 ^ (n + 2) - sin (π / 2 ^ (n + 2)) < (π / 2 ^ (n + 2)) ^ 3 / 4 :=
    sub_lt_comm.1 <| sin_gt_sub_cube (by positivity) <| div_le_one_of_le₀ ?_ (by positivity)
  _ ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4 := by gcongr; exact pi_le_four
  _ = 1 / (2 ^ n) ^ 3 / 4 := by simp [add_comm n, pow_add, div_mul_eq_div_div]; norm_num

Result:
n : ℕ
⊢ π ≤ 2 ^ (n + 2)

Proof state:
n : ℕ
⊢ (4 / 2 ^ 2 / 2 ^ n) ^ 3 / 4 = ((2 ^ n) ^ 3)⁻¹ / 4

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ 4 = 2 ^ (0 + 2)

Tactic:
norm_num

Result:
no goals