awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
s : Finset ℕ
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
have refine : ∀ (p : ℕ) (hp : p ∈ {p ∈ s | Nat.Prime p}),
  ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n) = (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹
Tactic: refine prod_congr rfl fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
s : Finset ℕ
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
p : ℕ
hp : p ∈ {p ∈ s | Nat.Prime p}
⊢ ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n) = (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹
have simp : ∑' (n : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n =
  (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹
Tactic: simp only [map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
s : Finset ℕ
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑(factoredNumbers s) : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
have H₁ : Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
  (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
Tactic: have H₁ :
      ∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n) = ∏ p ∈ s with p.Prime, (1 - f p)⁻¹ := by
    refine prod_congr rfl fun p hp ↦ ?_
    simp only [map_pow]
    exact tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
s : Finset ℕ
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
p : ℕ
hp : Nat.Prime p
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) (p ^ n) : F)
have simp : Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n‖
Tactic: simp only [map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
s : Finset ℕ
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
p : ℕ
hp : Nat.Prime p
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n‖
have refine : Summable (HPow.hPow (norm (E := F) ((f : (a : ℕ) → F) p : F)))
Tactic: refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
s : Finset ℕ
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑(factoredNumbers s) : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
have H₂ : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) (p ^ n) : F)
Tactic: have H₂ : ∀ {p : ℕ}, p.Prime → Summable fun n ↦ ‖f (p ^ n)‖ := by
    intro p hp
    simp only [map_pow]
    refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_
    exact summable_geometric_iff_norm_lt_one.mpr <| (norm_norm (f p)).symm ▸ h hp
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
s : Finset ℕ
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑(factoredNumbers s) : Type)), (f : (a : ℕ) → F) (↑m : ℕ))
have refine : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
Tactic: refine (summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric ?_ s).2.tsum_eq.symm
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
N : ℕ
⊢ (Summable (α := ℝ) fun (m : (↑N.smoothNumbers : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑N.smoothNumbers : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ N.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
have rw : (Summable (α := ℝ) fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
  HasSum.{u_1, 0} (α := F) (fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
    (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
Tactic: rw [smoothNumbers_eq_factoredNumbers, primesBelow]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
N : ℕ
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ N.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑N.smoothNumbers : Type)), (f : (a : ℕ) → F) (↑m : ℕ))
have rw : Eq.{u_1 + 1} (α := F)
  (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
  (∑' (m : (↑(factoredNumbers (range N)) : Type)), (f : (a : ℕ) → F) (↑m : ℕ))
Tactic: rw [smoothNumbers_eq_factoredNumbers, primesBelow]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ HasProd.{u_1, 0} (α := F)
    (fun (p : Primes) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) (↑p : ℕ) : F))⁻¹)
    (∑' (n : ℕ), (f : (a : ℕ) → F) n)
have H : Eq.{u_1 + 1} (α := (p : Primes) → F)
  (fun (p : Primes) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) (↑p : ℕ) : F))⁻¹) fun (p : Primes) ↦
  ∑' (e : ℕ), (f : (a : ℕ) → F) ((↑p : ℕ) ^ e)
Tactic: have H : (fun p : Primes ↦ (1 - f p)⁻¹) = fun p : Primes ↦ ∑' (e : ℕ), f (p ^ e) :=
    funext <| fun p ↦ one_sub_inv_eq_geometric_of_summable_norm p.prop hsum
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) atTop
    (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
have hmul : ∀ {m n : ℕ},
  m.Coprime n →
    (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
Tactic: have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
⊢ Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) atTop
    (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
have this : Tendsto.{0, u_1} (β := F)
  (fun (n : ℕ) ↦
    ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)) i)
  atTop (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
Tactic: have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
this :
  Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦
      ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)) i)
    atTop (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
⊢ Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) atTop
    (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
have H : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := F)
    (∏ p ∈ range n,
      Set.mulIndicator {p : ℕ | Nat.Prime p}
        (fun (p : ℕ) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) p)
    (∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
Tactic: have H (n : ℕ) : ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p =
                     ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
    prod_mulIndicator_eq_prod_filter
      (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
this :
  Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦
      ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)) i)
    atTop (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
H :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := F)
      (∏ p ∈ range n,
        Set.mulIndicator {p : ℕ | Nat.Prime p}
          (fun (p : ℕ) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) p)
      (∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
⊢ Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) atTop
    (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
have H' : Eq.{u_1 + 1} (α := (x : ℕ) → F)
  (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦
    (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
  (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e))
Tactic: have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
              {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖
have h : ∀ (n : ℕ), ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
Tactic: convert! Real.summable_nat_rpow_inv.mpr hs with n
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
have h : ‖(↑(↑n : ℝ) : ℂ) ^ (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
Tactic: rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
h : ‖(↑(↑n : ℝ) : ℂ) ^ (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
have h₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
Tactic: rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
h : ‖(↑(↑n : ℝ) : ℂ) ^ (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
h₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
have h₂ : HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re) = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
Tactic: rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
h : ‖(↑(↑n : ℝ) : ℂ) ^ (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
h₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
h₂ : HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re) = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
have h₃ : (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
Tactic: rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (hypothesis)
Goal:
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n = riemannZeta s
have hsum : Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := ℂ) ((riemannZetaSummandHom sorry : (a : ℕ) → ℂ) n : ℂ)
Tactic: have hsum := summable_riemannZetaSummand hs
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := ℂ) ((riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n : ℂ)
⊢ ∑' (n : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n = riemannZeta s
have rw : Eq (α := ℂ) (∑' (b : ℕ), (riemannZetaSummandHom sorry : (a : ℕ) → ℂ) (b + 1))
  (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s)
Tactic: rw [zeta_eq_tsum_one_div_nat_add_one_cpow hs, hsum.of_norm.tsum_eq_zero_add, map_zero, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := ℂ) ((dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n : ℂ)
have simp : Summable (α := ℝ) fun (n : ℕ) ↦
  norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖
Tactic: simp only [dirichletSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, norm_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ HasProd (fun (p : Primes) ↦ (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))⁻¹) (riemannZeta s)
have rw : HasProd (α := ℂ) (fun (p : Primes) ↦ (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))⁻¹)
  (∑' (n : ℕ), (riemannZetaSummandHom sorry : (a : ℕ) → ℂ) n)
Tactic: rw [← tsum_riemannZetaSummand hs]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))⁻¹) atTop (𝓝 (riemannZeta s))
have rw : Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))⁻¹) atTop
  (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom sorry : (a : ℕ) → ℂ) n))
Tactic: rw [← tsum_riemannZetaSummand hs]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd
    (fun (p : Primes) ↦
      (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹)
    (L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s)
have rw : HasProd (α := ℂ)
  (fun (p : Primes) ↦
    (1 -
        HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
          (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹)
  (∑' (n : ℕ), (dirichletSummandHom χ sorry : (a : ℕ) → ℂ) n)
Tactic: rw [← tsum_dirichletSummand χ hs]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto
    (fun (n : ℕ) ↦
      ∏ p ∈ n.primesBelow,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
    atTop (𝓝 (L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s))
have rw : Tendsto (β := ℂ)
  (fun (n : ℕ) ↦
    ∏ p ∈ n.primesBelow,
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
  atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ sorry : (a : ℕ) → ℂ) n))
Tactic: rw [← tsum_dirichletSummand χ hs]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
⊢ term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n
have inl : term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s 0 = (f : (a : ℕ) → ℂ) 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
inl : term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s 0 = (f : (a : ℕ) → ℂ) 0
⊢ term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n
have inr : ∀ (hn : n ≠ 0), term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
⊢ cexp
      (∑' (p : Primes),
        -Complex.log
            (1 -
              HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))) =
    L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
have h : ∀ (n : ℕ), term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n
Tactic: have h n : term ↗χ s n = f n := by
    rcases eq_or_ne n 0 with rfl | hn
    · simp only [term_zero, map_zero]
    · simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, div_eq_mul_inv,
        dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, f]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -Complex.log (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))) = L 1 s
have h : ∀ (x : Primes),
  HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑(↑x : ℕ) : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s))
Tactic: convert!
    modOne_eq_one (R := ℂ) ▸
      DirichletCharacter.LSeries_eulerProduct_exp_log (1 : DirichletCharacter ℂ 1) hs using 7
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
x : Primes
⊢ HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑(↑x : ℕ) : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s))
have h : HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) = 1 * HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s)
Tactic: rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.DirichletLSeries (goal)
Goal:
s : ℂ
hs : 1 < s.re
x : Primes
h : HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) = 1 * HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s)
⊢ HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑(↑x : ℕ) : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s))
have h₁ : HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) = HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s)
Tactic: rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_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
⊢ 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)))
have 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)
Tactic: rw [prod_eq_tprod_mulIndicator, ← DirichletCharacter.LSeries_eulerProduct_tprod _ hs,
    ← DirichletCharacter.LSeries_eulerProduct_tprod _ hs]