awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (hypothesis)
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ ∏' (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)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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 : 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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))
⊢ ∏' (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)
have hf : Multipliable (α := ℂ)
  (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦
    (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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)))⁻¹)
⊢ ∏' (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)
have hg : Multipliable (α := ℂ)
  ((↑N.primeFactors : Set ℕ).mulIndicator fun (p : ℕ) ↦
    1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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)
⊢ 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))
have 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)
Tactic: congr 1 with p
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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 : ℕ
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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 : ℕ
⊢ (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
have 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
Tactic: by_cases h : p.Prime
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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
⊢ (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
have 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
Tactic: by_cases h : p.Prime
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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
have 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)))⁻¹
Tactic: simp only [h, true_and, if_true]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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
⊢ (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)))⁻¹
have 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)))⁻¹
Tactic: by_cases hp' : p ∣ N
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
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)))⁻¹
⊢ (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)))⁻¹
have 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)))⁻¹
Tactic: by_cases hp' : p ∣ N