-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Modified version of `hasSum_int_evenKernel` omitting the constant term at `∞`. -/
lemma hasSum_int_evenKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) :
    HasSum (fun n : ℤ ↦ if n + a = 0 then 0 else rexp (-π * (n + a) ^ 2 * t))
    (evenKernel a t - if (a : UnitAddCircle) = 0 then 1 else 0)

Proof state:
a t : ℝ
ht : 0 < t
this✝ : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
this : ∀ (n : ℤ), ↑n + a ≠ 0
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Tactic:
simpa [this] using hasSum_int_evenKernel a ht

Result:
no goals

Proof state:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ ∀ (n : ℤ), ↑n + a ≠ 0

Tactic:
contrapose! h

Result:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n + a = 0
⊢ ∃ n, ↑n = a

Proof state:
case pos
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n = a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 1)

Tactic:
obtain ⟨k, rfl⟩ := h

Result:
case pos.intro
t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
k : ℤ
⊢ HasSum (fun n => if ↑n + ↑k = 0 then 0 else rexp (-π * (↑n + ↑k) ^ 2 * t)) (evenKernel (↑↑k) t - 1)

Proof state:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Tactic:
simp_rw [AddCircle.coe_eq_zero_iff, zsmul_one]

Result:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t))
    (evenKernel (↑a) t - if ∃ n, ↑n = a then 1 else 0)

Proof state:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n + a = 0
n : ℤ
hn : ↑n + a = 0
⊢ ∃ n, ↑n = a

Tactic:
exact ⟨-n, by simpa [neg_eq_iff_add_eq_zero]⟩

Result:
no goals

Proof state:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Tactic:
suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht

Result:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ ∀ (n : ℤ), ↑n + a ≠ 0

Proof state:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t))
    (evenKernel (↑a) t - if ∃ n, ↑n = a then 1 else 0)

Tactic:
split_ifs with h

Result:
case pos
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n = a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 1)

case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Proof state:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n + a = 0
⊢ ∃ n, ↑n = a

Tactic:
let ⟨n, hn⟩ := h

Result:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n + a = 0
n : ℤ
hn : ↑n + a = 0
⊢ ∃ n, ↑n = a

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Tactic:
haveI := Classical.propDecidable

Result:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Proof state:
case pos.intro
t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
k : ℤ
⊢ HasSum (fun n => if ↑n + ↑k = 0 then 0 else rexp (-π * (↑n + ↑k) ^ 2 * t)) (evenKernel (↑↑k) t - 1)

Tactic:
simpa [← Int.cast_add, add_eq_zero_iff_eq_neg]
  using hasSum_ite_sub_hasSum (hasSum_int_evenKernel (k : ℝ) ht) (-k)

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n + a = 0
n : ℤ
hn : ↑n + a = 0
⊢ ↑(-n) = a

Tactic:
simpa [neg_eq_iff_add_eq_zero]

Result:
no goals