-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
lemma abscissaOfAbsConv_residueClass_le_one :
    abscissaOfAbsConv ↗(residueClass a) ≤ 1

Proof state:
case h.e'_5.h
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
n : ℕ
⊢ term (fun n => ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y) n

Tactic:
by_cases hn : (n : ZMod q) = a

Result:
case pos
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
n : ℕ
hn : ↑n = a
⊢ term (fun n => ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y) n

case neg
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
n : ℕ
hn : ¬↑n = a
⊢ term (fun n => ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y) n

Proof state:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
⊢ Summable (term (fun n => ↑(residueClass a n)) ↑y)

Tactic:
convert this.indicator {n : ℕ | (n : ZMod q) = a}

Result:
case h.e'_5
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
⊢ term (fun n => ↑(residueClass a n)) ↑y = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y)

Proof state:
case h.e'_5
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
⊢ term (fun n => ↑(residueClass a n)) ↑y = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y)

Tactic:
ext1 n

Result:
case h.e'_5.h
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
n : ℕ
⊢ term (fun n => ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y) n

Proof state:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ 1 < (↑y).re

Tactic:
simp only [ofReal_re, hy]

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ LSeriesSummable (fun n => ↑(residueClass a n)) ↑y

Tactic:
unfold LSeriesSummable

Result:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ Summable (term (fun n => ↑(residueClass a n)) ↑y)

Proof state:
q : ℕ
a : ZMod q
⊢ (abscissaOfAbsConv fun n => ↑(residueClass a n)) ≤ 1

Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable fun y hy ↦ ?_

Result:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ LSeriesSummable (fun n => ↑(residueClass a n)) ↑y

Proof state:
case pos
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
n : ℕ
hn : ↑n = a
⊢ term (fun n => ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y) n

Tactic:
simp +contextual only [term, Set.indicator, Set.mem_setOf_eq, hn, ↓reduceIte, apply_ite,
  ite_self]

Result:
no goals

Proof state:
case neg
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
n : ℕ
hn : ¬↑n = a
⊢ term (fun n => ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n => ↑(Λ n)) ↑y) n

Tactic:
simp +contextual only [term, Set.mem_setOf_eq, hn, not_false_eq_true, Set.indicator_of_not_mem,
  ofReal_zero, zero_div, ite_self]

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ Summable (term (fun n => ↑(residueClass a n)) ↑y)

Tactic:
have := LSeriesSummable_vonMangoldt <| show 1 < (y : ℂ).re by simp only [ofReal_re, hy]

Result:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n => ↑(Λ n)) ↑y
⊢ Summable (term (fun n => ↑(residueClass a n)) ↑y)