awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
rw :
  ∏' (p : Primes),
      (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑(↑p : ℕ) : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹ =
    HMul.hMul (α := ℂ)
      (∏' (p : Primes),
        (1 -
            HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑(↑p : ℕ) : ZMod M) : ℂ)
              (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹)
      (∏' (x : ℕ),
        (↑N.primeFactors : Set ℕ).mulIndicator
          (fun (p : ℕ) ↦
            1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
          x)
⊢ L
      (fun (n : ℕ) ↦
        (((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
            (a : ZMod N) → ℂ)
          (↑n : ZMod N))
      s =
    L (fun (n : ℕ) ↦ (χ : (a : ZMod M) → ℂ) (↑n : ZMod M)) s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

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

Premises used: DirichletCharacter.LSeries_eulerProduct_tprod, prod_eq_tprod_mulIndicator, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)

Tactic:
have (f : Primes → ℂ) : ∏' (p : Primes), f p = ∏' (p : ↑{p : ℕ | p.Prime}), f p := rfl
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
rw :
  Eq (α := ℂ)
    (∏' (x : ℕ),
      Set.mulIndicator {p : ℕ | Nat.Prime p}
        (fun (p : ℕ) ↦
          (1 -
              HMul.hMul (α := ℂ)
                ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ :
                        DirichletCharacter ℂ N) :
                      (a : ZMod N) → ℂ)
                    (↑p : ZMod N) :
                  ℂ)
                (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
        x)
    (∏' (b : ℕ),
      HMul.hMul (α := ℂ)
        (Set.mulIndicator {p : ℕ | Nat.Prime p}
          (fun (p : ℕ) ↦
            (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
          b)
        ((↑N.primeFactors : Set ℕ).mulIndicator
          (fun (p : ℕ) ↦
            1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
          b))
hf :
  Multipliable (α := ℂ)
    (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
hg :
  Multipliable (α := ℂ)
    ((↑N.primeFactors : Set ℕ).mulIndicator fun (p : ℕ) ↦
      1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
⊢ ∏' (p : Primes),
      (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑(↑p : ℕ) : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹ =
    HMul.hMul (α := ℂ)
      (∏' (p : Primes),
        (1 -
            HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑(↑p : ℕ) : ZMod M) : ℂ)
              (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹)
      (∏' (x : ℕ),
        (↑N.primeFactors : Set ℕ).mulIndicator
          (fun (p : ℕ) ↦
            1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑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))⁻¹, ← Multipliable.tprod_mul]

Premises used: HMul.hMul, HSub.hSub, Nat.cast, Inv.inv, HPow.hPow, tprod_subtype, DirichletCharacter.changeLevel, Multipliable.tprod_mul, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
⊢ Multipliable (α := ℂ)
    (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)

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

Premises used: multipliable_subtype_iff_mulIndicator, DirichletCharacter.LSeries_eulerProduct_hasProd, Iff.mp, HasProd.multipliable
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
⊢ Multipliable (α := ℂ)
    (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)

Tactic:
exact multipliable_subtype_iff_mulIndicator.mp
      (DirichletCharacter.LSeries_eulerProduct_hasProd χ hs).multipliable
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
⊢ Multipliable (α := ℂ)
    ((↑N.primeFactors : Set ℕ).mulIndicator fun (p : ℕ) ↦
      1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
multipliable_subtype_iff_mulIndicator.mp Multipliable.of_finite

Premises used: multipliable_subtype_iff_mulIndicator, Multipliable.of_finite, Iff.mp
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
⊢ Multipliable (α := ℂ)
    ((↑N.primeFactors : Set ℕ).mulIndicator fun (p : ℕ) ↦
      1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
exact multipliable_subtype_iff_mulIndicator.mp Multipliable.of_finite

Premises used: multipliable_subtype_iff_mulIndicator, Multipliable.of_finite, Iff.mp
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
e_f :
  ∀ (p : ℕ),
    Set.mulIndicator {p : ℕ | Nat.Prime p}
        (fun (p : ℕ) ↦
          (1 -
              HMul.hMul (α := ℂ)
                ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ :
                        DirichletCharacter ℂ N) :
                      (a : ZMod N) → ℂ)
                    (↑p : ZMod N) :
                  ℂ)
                (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
        p =
      HMul.hMul (α := ℂ)
        (Set.mulIndicator {p : ℕ | Nat.Prime p}
          (fun (p : ℕ) ↦
            (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
          p)
        ((↑N.primeFactors : Set ℕ).mulIndicator
          (fun (p : ℕ) ↦
            1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
          p)
⊢ Eq (α := ℂ)
    (∏' (x : ℕ),
      Set.mulIndicator {p : ℕ | Nat.Prime p}
        (fun (p : ℕ) ↦
          (1 -
              HMul.hMul (α := ℂ)
                ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ :
                        DirichletCharacter ℂ N) :
                      (a : ZMod N) → ℂ)
                    (↑p : ZMod N) :
                  ℂ)
                (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
        x)
    (∏' (b : ℕ),
      HMul.hMul (α := ℂ)
        (Set.mulIndicator {p : ℕ | Nat.Prime p}
          (fun (p : ℕ) ↦
            (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
          b)
        ((↑N.primeFactors : Set ℕ).mulIndicator
          (fun (p : ℕ) ↦
            1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
          b))

Tactic:
congr 1 with p
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
e_f :
  (if Nat.Prime p then
      (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑p : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
    else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
      else 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
    else
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
      else 1
⊢ Set.mulIndicator {p : ℕ | Nat.Prime p}
      (fun (p : ℕ) ↦
        (1 -
            HMul.hMul (α := ℂ)
              ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                    (a : ZMod N) → ℂ)
                  (↑p : ZMod N) :
                ℂ)
              (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
      p =
    HMul.hMul (α := ℂ)
      (Set.mulIndicator {p : ℕ | Nat.Prime p}
        (fun (p : ℕ) ↦
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
        p)
      ((↑N.primeFactors : Set ℕ).mulIndicator
        (fun (p : ℕ) ↦
          1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑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]

Premises used: Set.mulIndicator_apply, mul_ite, Set.mem_setOf_eq, ne_eq, ite_mul, mul_one, Finset.mem_coe, Nat.mem_primeFactors, one_mul
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
pos :
  ∀ (h : Nat.Prime p),
    (if Nat.Prime p then
        (1 -
            HMul.hMul (α := ℂ)
              ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                    (a : ZMod N) → ℂ)
                  (↑p : ZMod N) :
                ℂ)
              (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
      else 1) =
      if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then
        if Nat.Prime p then
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
            (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
        else 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
      else
        if Nat.Prime p then
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
        else 1
neg :
  ∀ (h : ¬Nat.Prime p),
    (if Nat.Prime p then
        (1 -
            HMul.hMul (α := ℂ)
              ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                    (a : ZMod N) → ℂ)
                  (↑p : ZMod N) :
                ℂ)
              (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
      else 1) =
      if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then
        if Nat.Prime p then
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
            (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
        else 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
      else
        if Nat.Prime p then
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
        else 1
⊢ (if Nat.Prime p then
      (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑p : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
    else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
      else 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
    else
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
      else 1

Tactic:
by_cases h : p.Prime

Premises used: Nat.Prime
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : ¬Nat.Prime p
⊢ (if Nat.Prime p then
      (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑p : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
    else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
      else 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
    else
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
      else 1

Tactic:
simp only [h, false_and, if_false]

Premises used: if_false, false_and
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
pos :
  (1 -
        HMul.hMul (α := ℂ)
          ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                (a : ZMod N) → ℂ)
              (↑p : ZMod N) :
            ℂ)
          (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
    else (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
⊢ (if Nat.Prime p then
      (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑p : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
    else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
      else 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
    else
      if Nat.Prime p then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
      else 1

Tactic:
simp only [h, true_and, if_true]

Premises used: if_true, true_and
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
pos :
  ∀ (hp' : p ∣ N),
    (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑p : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
      if p ∣ N ∧ ¬N = 0 then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
      else (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
neg :
  ∀ (hp' : ¬p ∣ N),
    (1 -
          HMul.hMul (α := ℂ)
            ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                  (a : ZMod N) → ℂ)
                (↑p : ZMod N) :
              ℂ)
            (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
      if p ∣ N ∧ ¬N = 0 then
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
      else (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹
⊢ (1 -
        HMul.hMul (α := ℂ)
          ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                (a : ZMod N) → ℂ)
              (↑p : ZMod N) :
            ℂ)
          (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
    else (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹

Tactic:
by_cases hp' : p ∣ N
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
neg :
  Eq (α := ℂ)
    ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
          (a : ZMod N) → ℂ)
        (↑p : ZMod N) :
      ℂ)
    ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ)
⊢ (1 -
        HMul.hMul (α := ℂ)
          ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                (a : ZMod N) → ℂ)
              (↑p : ZMod N) :
            ℂ)
          (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
    else (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑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]

Premises used: sub_right_inj, false_and, Complex.cpow_eq_zero_iff, neg_eq_zero, mul_eq_mul_right_iff, ne_eq, inv_inj, Nat.cast_eq_zero, Nat.Prime.ne_zero, reduceIte, or_false
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
⊢ IsUnit (M := ZMod N) (↑p : ZMod N)

Tactic:
have hq : IsUnit (p : ZMod N) := (ZMod.isUnit_prime_iff_not_dvd h).mpr hp'
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
hq : IsUnit (M := ZMod N) (↑p : ZMod N)
⊢ Eq (α := ℂ)
    ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
          (a : ZMod N) → ℂ)
        (↑p : ZMod N) :
      ℂ)
    ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ)

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

Premises used: ZMod.cast_natCast
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
pos :
  (1 -
        HMul.hMul (α := ℂ)
          ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                (a : ZMod N) → ℂ)
              (↑p : ZMod N) :
            ℂ)
          (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
    (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
⊢ (1 -
        HMul.hMul (α := ℂ)
          ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                (a : ZMod N) → ℂ)
              (↑p : ZMod N) :
            ℂ)
          (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
    else (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹

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

Premises used: and_self, reduceIte, not_false_eq_true, NeZero.ne