k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ W k
rw [← le_div_iff pi_div_two_pos, div_eq_inv_mul (W k) _]
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff (integral_sin_pow_pos _)]
case h.e'_3
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1 + 1)
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
convert integral_sin_pow_succ_le (2 * k + 1)
case h.e'_3
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
case h.e'_3
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1 + 1)
rw [integral_sin_pow (2 * k)]
case h.e'_3
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
case h.e'_3
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
simp only [sin_zero, zero_pow', Ne.def, Nat.succ_ne_zero, zero_mul, sin_pi, tsub_zero, zero_div,
  zero_add]
no goals
case h.e'_3
k : ℕ
⊢ ((2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
norm_cast