awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
p : Nat.Primes
k : ℕ
| f ((↑p : ℕ) ^ (k + 1 + 1))
have h : f ((↑p : ℕ) ^ (k + 2))
Tactic: rw [add_assoc, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
| ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1))
have h : ∀ (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2))
Tactic: enter [1, p]; rw [(hfs' p).tprod_eq_zero_mul, zero_add, pow_one]
    enter [2, 1, k]; rw [add_assoc, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
⊢ ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)) =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))
have conv_lhs : ∏' (p : Nat.Primes), f (↑p : ℕ) * ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 2)) =
  HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))
Tactic: conv_lhs =>
    enter [1, p]; rw [(hfs' p).tprod_eq_zero_mul, zero_add, pow_one]
    enter [2, 1, k]; rw [add_assoc, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) ≤ 1
have refine : ∀ (y : ℝ) (hy : 1 < y), LSeriesSummable (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ)
Tactic: refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ Summable (term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ))
have this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
Tactic: have := LSeriesSummable_vonMangoldt <| show 1 < (y : ℂ).re by simp only [ofReal_re, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
⊢ Summable (term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ))
have h : term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) =
  Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ))
Tactic: convert! this.indicator {n : ℕ | (n : ZMod q) = a}
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ))
have h : ∀ (n : ℕ),
  term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
n : ℕ
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
have pos : ∀ (hn : (↑n : ZMod q) = a),
  term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
Tactic: by_cases hn : (n : ZMod q) = a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
n : ℕ
pos :
  ∀ (hn : (↑n : ZMod q) = a),
    term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
      Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
have neg : ∀ (hn : ¬(↑n : ZMod q) = a),
  term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
Tactic: by_cases hn : (n : ZMod q) = a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
⊢ Eq (α := Set ℕ) (Function.support (M := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ))
    {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a}
have simp : Eq (α := Set ℕ) {x : ℕ | (Nat.Prime x ∧ (↑x : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)) ∧ ¬x = 0}
  {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a}
Tactic: simp only [Function.support, ne_eq, div_eq_zero_iff, ite_eq_right_iff,
    Set.indicator_apply_eq_zero, Set.mem_setOf_eq, Nat.cast_eq_zero, not_or, Classical.not_imp]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
⊢ Eq (α := Set ℕ) {x : ℕ | (Nat.Prime x ∧ (↑x : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)) ∧ ¬x = 0}
    {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a}
have h : ∀ (p : ℕ),
  Membership.mem (γ := Set ℕ)
      {x : ℕ | (Nat.Prime x ∧ (↑x : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)) ∧ ¬x = 0} p ↔
    Membership.mem (γ := Set ℕ) {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a} p
Tactic: ext1 p
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
p : Nat.Primes
k : ℕ
⊢ LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
have this : 0 < (↑p : ℕ)
Tactic: have := p.prop.pos
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
p : Nat.Primes
k : ℕ
⊢ 2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (-1 / 2) * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (k + 2) =
    2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ ((↑k : ℝ) + 3 / 2)
have rw : 2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ ((↑k : ℝ) + (2 + -1 / 2)) =
  2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ ((↑k : ℝ) + 3 / 2)
Tactic: rw [mul_assoc, ← Real.rpow_natCast,
        ← Real.rpow_add <| by have := p.prop.pos; positivity, Nat.cast_add, Nat.cast_two,
        add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
⊢ Summable F''
have hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
Tactic: have hp₀ (p : Nat.Primes) : 0 < (p : ℝ)⁻¹ := inv_pos_of_pos (Nat.cast_pos.mpr p.prop.pos)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
⊢ Summable F''
have hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
Tactic: have hp₁ (p : Nat.Primes) : (p : ℝ)⁻¹ < 1 :=
    (inv_lt_one₀ <| mod_cast p.prop.pos).mpr <| Nat.one_lt_cast.mpr <| p.prop.one_lt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
this : Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ F'' pk
have simp : 0 ≤
  HDiv.hDiv (α := ℝ)
    (if Nat.Prime ((↑pk.1 : ℕ) ^ (pk.2 + 1 + 1)) then 0 else (Λ : (a : ℕ) → ℝ) ((↑pk.1 : ℕ) ^ (pk.2 + 1 + 1)) : ℝ)
    (HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ) (pk.2 + 1 + 1))
Tactic: simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
this : Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤
    HDiv.hDiv (α := ℝ)
      (if Nat.Prime ((↑pk.1 : ℕ) ^ (pk.2 + 1 + 1)) then 0 else (Λ : (a : ℕ) → ℝ) ((↑pk.1 : ℕ) ^ (pk.2 + 1 + 1)) : ℝ)
      (HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ) (pk.2 + 1 + 1))
have positivity : LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) ((↑pk.1 : ℕ) ^ (pk.2 + 2)) : ℝ) →
  0 ≤
    HDiv.hDiv (α := ℝ)
      (if Nat.Prime ((↑pk.1 : ℕ) ^ (pk.2 + 1 + 1)) then 0 else (Λ : (a : ℕ) → ℝ) ((↑pk.1 : ℕ) ^ (pk.2 + 1 + 1)) : ℝ)
      (HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ) (pk.2 + 1 + 1))
Tactic: positivity [vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
⊢ Summable F''
have suffices : Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
Tactic: suffices Summable fun (pk : Nat.Primes × ℕ) ↦ (pk.1 : ℝ)⁻¹ ^ (pk.2 + 3 / 2 : ℝ) by
    refine (Summable.mul_left 2 this).of_nonneg_of_le (fun pk ↦ ?_) (fun pk ↦ F''_le pk.1 pk.2)
    simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]
    positivity [vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
| Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
have h : ∀ (pk : Nat.Primes × ℕ), HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
Tactic: enter [1, pk]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
pk : Nat.Primes × ℕ
| HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
have h : HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
| Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
have h : ∀ (pk : Nat.Primes × ℕ), HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: enter [1, pk]; rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
⊢ Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
have conv : Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦
  HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: conv => enter [1, pk]; rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
⊢ Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦
    HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
have refine_1 : ∀ (p : Nat.Primes),
  Summable (α := ℝ) fun (y : ℕ) ↦
    HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (p, y).2 * HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: refine (summable_prod_of_nonneg (fun _ ↦ by positivity)).mpr ⟨(fun p ↦ ?_), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
refine_1 :
  ∀ (p : Nat.Primes),
    Summable (α := ℝ) fun (y : ℕ) ↦
      HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (p, y).2 * HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (3 / 2)
⊢ Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦
    HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
have refine_2 : Summable (α := ℝ) fun (x : Nat.Primes) ↦
  ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑(x, y).1 : ℕ) : ℝ)⁻¹ (x, y).2 * HPow.hPow (α := ℝ) (↑(↑(x, y).1 : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: refine (summable_prod_of_nonneg (fun _ ↦ by positivity)).mpr ⟨(fun p ↦ ?_), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ Summable (α := ℝ) fun (y : ℕ) ↦
    HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (p, y).2 * HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (3 / 2)
have refine_1 : Summable (α := ℝ) fun (y : ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
| Summable (α := ℝ) fun (x : Nat.Primes) ↦
    ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ (3 / 2)
have h : ∀ (p : Nat.Primes), ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: enter [1, p]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
| ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
have h : (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
| Summable (α := ℝ) fun (x : Nat.Primes) ↦
    ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ (3 / 2)
have h : ∀ (p : Nat.Primes), (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: enter [1, p]; rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
⊢ Summable (α := ℝ) fun (x : Nat.Primes) ↦
    ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ (3 / 2)
have refine_2 : Summable (α := ℝ) fun (p : Nat.Primes) ↦
  (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: conv => enter [1, p]; rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
⊢ Summable (α := ℝ) fun (p : Nat.Primes) ↦
    (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
have refine_2 : ∀ (p : Nat.Primes), 0 ≤ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: refine (summable_rpow.mpr (by norm_num : -(3 / 2 : ℝ) < -1)).mul_left 2
      |>.of_nonneg_of_le (fun p ↦ ?_) (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
refine_2 :
  ∀ (p : Nat.Primes), 0 ≤ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
⊢ Summable (α := ℝ) fun (p : Nat.Primes) ↦
    (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
have refine_2₁ : ∀ (p : Nat.Primes),
  (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2) ≤
    2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-(3 / 2))
Tactic: refine (summable_rpow.mpr (by norm_num : -(3 / 2 : ℝ) < -1)).mul_left 2
      |>.of_nonneg_of_le (fun p ↦ ?_) (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ 0 ≤ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
have refine_2 : 0 < HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹ →
  0 ≤ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
Tactic: positivity [sub_pos.mpr (hp₁ p)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2) ≤
    2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-(3 / 2))
have refine_2 : (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 2))⁻¹ ≤
  2 * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 2))⁻¹
Tactic: rw [Real.inv_rpow p.val.cast_nonneg, Real.rpow_neg p.val.cast_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 2))⁻¹ ≤
    2 * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 2))⁻¹
have refine_2 : (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ ≤ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ ≤ 2
have refine_2 : LE.le (α := ℝ) 2 (↑(↑p : ℕ) : ℝ)
Tactic: rw [inv_le_comm₀ (sub_pos.mpr (hp₁ p)) zero_lt_two, le_sub_comm,
        show (1 : ℝ) - 2⁻¹ = 2⁻¹ by norm_num, inv_le_inv₀ (mod_cast p.prop.pos) zero_lt_two]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
n : ℕ
⊢ 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
have positivity : 0 ≤ residueClass a n → 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
Tactic: positivity [residueClass_nonneg a n]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
a : ZMod q
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
have h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
Tactic: have h₀ (n : ℕ) : 0 ≤ (if n.Prime then 0 else residueClass a n) / n := by
    positivity [residueClass_nonneg a n]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
n : ℕ
⊢ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n
have refine : (if Nat.Prime n then 0 else residueClass a n) ≤ if Nat.Prime n then 0 else (Λ : (a : ℕ) → ℝ) n
Tactic: refine div_le_div_of_nonneg_right ?_ n.cast_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
n : ℕ
⊢ (if Nat.Prime n then 0 else residueClass a n) ≤ if Nat.Prime n then 0 else (Λ : (a : ℕ) → ℝ) n
have pos : Nat.Prime n → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
n : ℕ
pos : Nat.Prime n → LE.le (α := ℝ) 0 0
⊢ (if Nat.Prime n then 0 else residueClass a n) ≤ if Nat.Prime n then 0 else (Λ : (a : ℕ) → ℝ) n
have neg : ¬Nat.Prime n → residueClass a n ≤ (Λ : (a : ℕ) → ℝ) n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
have hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n
Tactic: have hleF₀ (n : ℕ) : (if n.Prime then 0 else residueClass a n) / n ≤ F₀ n := by
    refine div_le_div_of_nonneg_right ?_ n.cast_nonneg
    split_ifs; exacts [le_rfl, residueClass_le a n]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
have refine : Summable F₀
Tactic: refine Summable.of_nonneg_of_le h₀ hleF₀ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n
⊢ Summable F₀
have hF₀ : ∀ (p : Nat.Primes), F₀ (↑p : ℕ) = 0
Tactic: have hF₀ (p : Nat.Primes) : F₀ p.val = 0 := by
    simp only [p.prop, ↓reduceIte, zero_div, F₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ (↑p : ℕ) = 0
⊢ Summable F₀
have refine_1 : Summable (β := (↑{n : ℕ | IsPrimePow n} : Type))
  (F₀ ∘ Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} x))
Tactic: refine (summable_subtype_iff_indicator (s := {n | IsPrimePow n}).mp ?_).congr
      fun n ↦ Set.indicator_apply_eq_self.mpr fun (hn : ¬ IsPrimePow n) ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ (↑p : ℕ) = 0
refine_1 :
  Summable (β := (↑{n : ℕ | IsPrimePow n} : Type))
    (F₀ ∘ Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} x))
⊢ Summable F₀
have refine_2 : ∀ (n : ℕ) (hn : ¬IsPrimePow n), F₀ n = 0
Tactic: refine (summable_subtype_iff_indicator (s := {n | IsPrimePow n}).mp ?_).congr
      fun n ↦ Set.indicator_apply_eq_self.mpr fun (hn : ¬ IsPrimePow n) ↦ ?_