-- Mathlib/NumberTheory/ZetaValues.lean
theorem hasSum_L_function_mod_four_eval_three :
    HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 3 * Real.sin (π * n / 2)) (π ^ 3 / 32)

Proof state:
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32

Tactic:
have : (1 / 4 : ℝ) = (algebraMap ℚ ℝ) (1 / 4 : ℚ) := by norm_num

Result:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32

Proof state:
case h.h.e_x
n : ℕ
⊢ 2 * π * ↑n * (1 / 4) = π * ↑n / 2

Tactic:
ring

Result:
no goals

Proof state:
case h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2) ∨ n = 0

Tactic:
left

Result:
case h.h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2)

Proof state:
case right

⊢ 1 / 4 ≤ 1

Tactic:
linarith

Result:
no goals

Proof state:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32

Tactic:
rw [this, mul_pow, Polynomial.eval_map, Polynomial.eval₂_at_apply, (by decide : 2 * 1 + 1 = 3),
  Polynomial.bernoulli_three_eval_one_quarter]

Result:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 ^ 3 * π ^ 3) / 2 / ↑3! * (algebraMap ℚ ℝ) (3 / 64) = π ^ 3 / 32

Proof state:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 / 2 / 6 * (3 / 64) = π ^ 3 / 32

Tactic:
field_simp

Result:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 * 3 * 32 = π ^ 3 * (2 * 6 * 64)

Proof state:
⊢ 1 / 4 ∈ Icc 0 1

Tactic:
rw [mem_Icc]

Result:
⊢ 0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1

Proof state:
⊢ 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ HasSum (fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)) (π ^ 3 / 32)

Tactic:
apply (congr_arg₂ HasSum ?_ ?_).to_iff.mp <|
  hasSum_one_div_nat_pow_mul_sin one_ne_zero (?_ : 1 / 4 ∈ Icc (0 : ℝ) 1)

Result:
⊢ (fun n => 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4))) = fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)


⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32


⊢ 1 / 4 ∈ Icc 0 1

Proof state:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 * 3 * 32 = π ^ 3 * (2 * 6 * 64)

Tactic:
ring

Result:
no goals

Proof state:
case h.h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2)

Tactic:
congr 1

Result:
case h.h.e_x
n : ℕ
⊢ 2 * π * ↑n * (1 / 4) = π * ↑n / 2

Proof state:
⊢ 0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1

Tactic:
constructor

Result:
case left

⊢ 0 ≤ 1 / 4

case right

⊢ 1 / 4 ≤ 1

Proof state:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ 2 * 1 + 1 = 3

Tactic:
decide

Result:
no goals

Proof state:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 ^ 3 * π ^ 3) / 2 / ↑3! * (algebraMap ℚ ℝ) (3 / 64) = π ^ 3 / 32

Tactic:
norm_num [Nat.factorial]

Result:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 / 2 / 6 * (3 / 64) = π ^ 3 / 32

Proof state:
⊢ (fun n => 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4))) = fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)

Tactic:
ext1 n

Result:
case h
n : ℕ
⊢ 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4)) = 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)

Proof state:
case left

⊢ 0 ≤ 1 / 4

Tactic:
linarith

Result:
no goals

Proof state:
case h
n : ℕ
⊢ 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4)) = 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)

Tactic:
norm_num

Result:
case h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2) ∨ n = 0