-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem completedZeta_eq_tsum_of_one_lt_re {s : ℂ} (hs : 1 < re s) :
    completedRiemannZeta s =
      (π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ∑' n : ℕ, 1 / (n : ℂ) ^ s

Proof state:
case pos
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
h : n = 0
⊢ 0 = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

Tactic:
simp only [h, Nat.cast_zero, zero_cpow (Complex.ne_zero_of_one_lt_re hs), div_zero]

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
simp only [this, Gammaℝ_def, mul_zero, zero_mul, Real.cos_zero, ofReal_one, mul_one, mul_one_div,
  ← tsum_mul_left]

Result:
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ (∑' (b : ℕ), if b = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑b ^ s) =
    ∑' (x : ℕ), ↑π ^ (-s / 2) * Gamma (s / 2) / ↑x ^ s

Proof state:
case e_f.h
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
⊢ (if n = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s) = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

Tactic:
split_ifs with h

Result:
case pos
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
h : n = 0
⊢ 0 = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

case neg
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
h : ¬n = 0
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

Proof state:
s : ℂ
hs : 1 < s.re
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
have := (hasSum_nat_completedCosZeta 0 hs).tsum_eq.symm

Result:
s : ℂ
hs : 1 < s.re
this : completedCosZeta (↑0) s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Proof state:
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ (∑' (b : ℕ), if b = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑b ^ s) =
    ∑' (x : ℕ), ↑π ^ (-s / 2) * Gamma (s / 2) / ↑x ^ s

Tactic:
congr 1 with n

Result:
case e_f.h
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
⊢ (if n = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s) = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

Proof state:
s : ℂ
hs : 1 < s.re
this : completedCosZeta (↑0) s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
simp only [QuotientAddGroup.mk_zero, completedCosZeta_zero] at this

Result:
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Proof state:
case neg
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
h : ¬n = 0
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

Tactic:
rfl

Result:
no goals