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
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ π < a
refine' lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) _
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

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)

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)
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
rw [← le_sub_iff_add_le, ← le_div_iff', sqrt_le_left, sub_le_comm]
no goals
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
rwa [Nat.cast_zero, zero_div] at h
no goals
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)
exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)
no goals
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)
exact pow_pos zero_lt_two _