-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- If `s` is not of the form `1 - n` for `n ∈ ℕ`, then `cosZeta a (1 - s)` is an explicit
multiple of `hurwitzZetaEven s`. -/
lemma cosZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - n) :
    cosZeta a (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * cos (π * s / 2) * hurwitzZetaEven a s

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹

Tactic:
rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]

Result:
case h
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ 1 - s ≠ 0

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s

Tactic:
rw [this, completedCosZeta_one_sub, inv_Gammaℝ_one_sub (fun n ↦ by simpa using hs (n + 1)),
  hurwitzZetaEven_def_of_ne_or_ne (Or.inr (by simpa using hs 1))]

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos (↑π * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
n : ℕ
⊢ s ≠ -↑n

Tactic:
simpa using hs (n + 1)

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
A : ℂ
⊢ completedHurwitzZetaEven a s * (A * s.Gammaℝ⁻¹) = A * (completedHurwitzZetaEven a s / s.Gammaℝ)

Tactic:
ring_nf

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ cosZeta a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s

Tactic:
rw [← Gammaℂ]

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos (↑π * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)

Tactic:
generalize Gammaℂ s * cos (π * s / 2) = A

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
A : ℂ
⊢ completedHurwitzZetaEven a s * (A * s.Gammaℝ⁻¹) = A * (completedHurwitzZetaEven a s / s.Gammaℝ)

Proof state:
case h
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ 1 - s ≠ 0

Tactic:
simpa [sub_eq_zero] using (hs 0).symm

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ s ≠ 0

Tactic:
simpa using hs 1

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s

Tactic:
have : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (Gammaℝ (1 - s))⁻¹ := by
  rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]
  simpa [sub_eq_zero] using (hs 0).symm

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s