-- 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:
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))

Tactic:
exact multipliable_subtype_iff_mulIndicator.mp Multipliable.of_finite

Result:
no goals

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
⊢ (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

Tactic:
simp only [h, true_and, if_true]

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
⊢ (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))⁻¹

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
⊢ (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

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
⊢ (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

Tactic:
swap

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
⊢ (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

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
⊢ (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

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 : ℕ
⊢ (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

Tactic:
by_cases h : p.Prime

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
⊢ (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

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
⊢ (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

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ((changeLevel hMN) χ) ↑n) s = L (fun n => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
rw [prod_eq_tprod_mulIndicator, ← DirichletCharacter.LSeries_eulerProduct_tprod _ hs,
  ← DirichletCharacter.LSeries_eulerProduct_tprod _ hs]

Result:
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

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
⊢ (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', false_and, ↓reduceIte, inv_inj, sub_right_inj, mul_eq_mul_right_iff,
  cpow_eq_zero_iff, Nat.cast_eq_zero, h.ne_zero, ne_eq, neg_eq_zero, or_false]

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
⊢ ((changeLevel hMN) χ) ↑p = χ ↑p

Proof state:
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))⁻¹)

Tactic:
exact multipliable_subtype_iff_mulIndicator.mp
  (DirichletCharacter.LSeries_eulerProduct_hasProd χ hs).multipliable

Result:
no goals

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
this : ¬IsUnit ↑p
⊢ 1 = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))

Tactic:
refine (inv_mul_cancel₀ ?_).symm

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
this : ¬IsUnit ↑p
⊢ 1 - χ ↑p * ↑p ^ (-s) ≠ 0