-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The auxiliary function takes real values for real arguments `x > 1`. -/
lemma LFunctionResidueClassAux_real (ha : IsUnit a) {x : ℝ} (hx : 1 < x) :
    LFunctionResidueClassAux a x = (LFunctionResidueClassAux a x).re

Proof state:
case e_a.inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : n ≠ 0
⊢ term (fun n => ↑(residueClass a n)) (↑x) n = ↑(term (fun n => ↑(residueClass a n)) (↑x) n).re

Tactic:
simp only [term_of_ne_zero hn, ← ofReal_natCast n, ← ofReal_cpow n.cast_nonneg, ← ofReal_div,
  ofReal_re]

Result:
no goals

Proof state:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun n => ↑(residueClass a n)) (↑x) n =
    ↑(∑' (a_1 : ℕ), (term (fun n => ↑(residueClass a n)) (↑x) a_1).re)

Tactic:
push_cast

Result:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun n => ↑(residueClass a n)) (↑x) n =
    ∑' (a_1 : ℕ), ↑(term (fun n => ↑(residueClass a n)) (↑x) a_1).re

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ 1 < ↑(↑x).re

Tactic:
norm_cast

Result:
no goals

Proof state:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun n => ↑(residueClass a n)) (↑x) n =
    ∑' (a_1 : ℕ), ↑(term (fun n => ↑(residueClass a n)) (↑x) a_1).re

Tactic:
refine tsum_congr fun n ↦ ?_

Result:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
⊢ term (fun n => ↑(residueClass a n)) (↑x) n = ↑(term (fun n => ↑(residueClass a n)) (↑x) n).re

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ LFunctionResidueClassAux a ↑x = ↑(LFunctionResidueClassAux a ↑x).re

Tactic:
rw [eqOn_LFunctionResidueClassAux ha hx]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x =
    ↑((fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x).re

Proof state:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑q.totient)⁻¹ / (↑x - 1) = ↑((↑q.totient)⁻¹ / (↑x - 1)).re

Tactic:
rw [show (q.totient : ℂ) = (q.totient : ℝ) from rfl, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
  ← ofReal_div, ofReal_re]

Result:
no goals

Proof state:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n => ↑(residueClass a n)) ↑x = ↑(L (fun n => ↑(residueClass a n)) ↑x).re

Tactic:
rw [LSeries, re_tsum <| LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
  (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| by norm_cast]

Result:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun n => ↑(residueClass a n)) (↑x) n =
    ↑(∑' (a_1 : ℕ), (term (fun n => ↑(residueClass a n)) (↑x) a_1).re)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x =
    ↑((fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x).re

Tactic:
simp only [sub_re, ofReal_sub]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n => ↑(residueClass a n)) ↑x - (↑q.totient)⁻¹ / (↑x - 1) =
    ↑(L (fun n => ↑(residueClass a n)) ↑x).re - ↑((↑q.totient)⁻¹ / (↑x - 1)).re

Proof state:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
⊢ term (fun n => ↑(residueClass a n)) (↑x) n = ↑(term (fun n => ↑(residueClass a n)) (↑x) n).re

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case e_a.inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ term (fun n => ↑(residueClass a n)) (↑x) 0 = ↑(term (fun n => ↑(residueClass a n)) (↑x) 0).re

case e_a.inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : n ≠ 0
⊢ term (fun n => ↑(residueClass a n)) (↑x) n = ↑(term (fun n => ↑(residueClass a n)) (↑x) n).re

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n => ↑(residueClass a n)) ↑x - (↑q.totient)⁻¹ / (↑x - 1) =
    ↑(L (fun n => ↑(residueClass a n)) ↑x).re - ↑((↑q.totient)⁻¹ / (↑x - 1)).re

Tactic:
congr 1

Result:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n => ↑(residueClass a n)) ↑x = ↑(L (fun n => ↑(residueClass a n)) ↑x).re

case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑q.totient)⁻¹ / (↑x - 1) = ↑((↑q.totient)⁻¹ / (↑x - 1)).re

Proof state:
case e_a.inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ term (fun n => ↑(residueClass a n)) (↑x) 0 = ↑(term (fun n => ↑(residueClass a n)) (↑x) 0).re

Tactic:
simp only [term_zero, zero_re, ofReal_zero]

Result:
no goals