-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
/-- If `χ` is a Dirichlet character and its level `M` divides `N`, then we obtain the L-series
of `χ` considered as a Dirichlet character of level `N` from the L-series of `χ` by multiplying
with `∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))`. -/
lemma DirichletCharacter.LSeries_changeLevel {M N : ℕ} [NeZero N]
    (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : 1 < s.re) :
    LSeries ↗(changeLevel hMN χ) s =
      LSeries ↗χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (p : Primes), (1 - ((changeLevel hMN) χ) ↑↑p * ↑↑p ^ (-s))⁻¹ =
    (∏' (p : Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) *
      ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) x

Tactic:
rw [this, tprod_subtype _ fun p : ℕ ↦ (1 - (changeLevel hMN χ) p * p ^ (-s))⁻¹,
  this, tprod_subtype _ fun p : ℕ ↦ (1 - χ p * p ^ (-s))⁻¹, ← tprod_mul]

Result:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (x : ℕ), {p | Nat.Prime p}.mulIndicator (fun p => (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) x =
    ∏' (b : ℕ),
      {p | Nat.Prime p}.mulIndicator (fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹) b *
        (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) b

case hf
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ({p | Nat.Prime p}.mulIndicator fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹)

case hg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ((↑N.primeFactors).mulIndicator fun p => 1 - χ ↑p * ↑p ^ (-s))

Proof state:
case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹

Tactic:
simp only [hp', NeZero.ne N, not_false_eq_true, and_self, ↓reduceIte]

Result:
case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (x : ℕ), {p | Nat.Prime p}.mulIndicator (fun p => (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) x =
    ∏' (b : ℕ),
      {p | Nat.Prime p}.mulIndicator (fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹) b *
        (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) b

Tactic:
congr 1 with p

Result:
case e_f.h
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
⊢ {p | Nat.Prime p}.mulIndicator (fun p => (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) p =
    {p | Nat.Prime p}.mulIndicator (fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹) p *
      (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) p

Proof state:
case neg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
hq : IsUnit ↑p
⊢ ((changeLevel hMN) χ) ↑p = χ ↑p

Tactic:
simp only [hq.unit_spec ▸ DirichletCharacter.changeLevel_eq_cast_of_dvd χ hMN hq.unit,
  ZMod.cast_natCast hMN]

Result:
no goals

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ ¬IsUnit ↑p

Tactic:
rwa [ZMod.isUnit_prime_iff_not_dvd h, not_not]

Result:
no goals

Proof state:
case neg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
⊢ ((changeLevel hMN) χ) ↑p = χ ↑p

Tactic:
have hq : IsUnit (p : ZMod N) := (ZMod.isUnit_prime_iff_not_dvd h).mpr hp'

Result:
case neg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
hq : IsUnit ↑p
⊢ ((changeLevel hMN) χ) ↑p = χ ↑p

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
ha : ‖χ ↑p‖ ≤ 1
hb : ‖↑p ^ (-s)‖ ≤ 1 / 2
⊢ ‖χ ↑p‖ * ‖↑p ^ (-s)‖ ≠ 1

Tactic:
exact ((mul_le_mul ha hb (norm_nonneg _) zero_le_one).trans_lt (by norm_num)).ne

Result:
no goals

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ ∏' (p : Primes), (1 - ((changeLevel hMN) χ) ↑↑p * ↑↑p ^ (-s))⁻¹ =
    (∏' (p : Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) *
      ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) x

Tactic:
have (f : Primes → ℂ) : ∏' (p : Primes), f p = ∏' (p : ↑{p : ℕ | p.Prime}), f p := rfl

Result:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (p : Primes), (1 - ((changeLevel hMN) χ) ↑↑p * ↑↑p ^ (-s))⁻¹ =
    (∏' (p : Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) *
      ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) x

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
ha : ‖χ ↑p‖ ≤ 1
hb : ‖↑p ^ (-s)‖ ≤ 1 / 2
⊢ 1 * (1 / 2) < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case e_f.h
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
⊢ {p | Nat.Prime p}.mulIndicator (fun p => (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) p =
    {p | Nat.Prime p}.mulIndicator (fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹) p *
      (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) p

Tactic:
simp only [Set.mulIndicator_apply, Set.mem_setOf_eq, Finset.mem_coe, Nat.mem_primeFactors,
  ne_eq, mul_ite, ite_mul, one_mul, mul_one]

Result:
case e_f.h
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
⊢ (if Nat.Prime p then (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then
      if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else 1 - χ ↑p * ↑p ^ (-s)
    else if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1