awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
p : ℕ
⊢ (Nat.Prime p ∧ (↑p : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) p : ℝ) (0 : ℝ)) ∧ ¬p = 0 ↔
    Nat.Prime p ∧ (↑p : ZMod q) = a

Tactic:
⟨fun H ↦ ⟨H.1.1, H.1.2.1⟩,
    fun H ↦ ⟨⟨H.1, H.2, vonMangoldt_ne_zero_iff.mpr H.1.isPrimePow⟩, H.1.ne_zero⟩⟩

Premises used: Iff.mpr, ArithmeticFunction.vonMangoldt_ne_zero_iff, And.right, And.left, Nat.Prime.ne_zero, And.intro, Iff.intro, Nat.Prime.isPrimePow
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
p : ℕ
⊢ (Nat.Prime p ∧ (↑p : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) p : ℝ) (0 : ℝ)) ∧ ¬p = 0 ↔
    Nat.Prime p ∧ (↑p : ZMod q) = a

Tactic:
exact ⟨fun H ↦ ⟨H.1.1, H.1.2.1⟩,
    fun H ↦ ⟨⟨H.1, H.2, vonMangoldt_ne_zero_iff.mpr H.1.isPrimePow⟩, H.1.ne_zero⟩⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
p : Nat.Primes
k : ℕ
⊢ F'' (p, k) = Real.log (↑(↑p : ℕ) : ℝ) * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (k + 2)

Tactic:
simp only [F'', Function.comp_apply, F', F₀, Prod.map_apply, id_eq, le_add_iff_nonneg_left,
        zero_le, Nat.Prime.not_prime_pow, ↓reduceIte, vonMangoldt_apply_prime p.prop,
        vonMangoldt_apply_pow (Nat.zero_ne_add_one _).symm, Nat.cast_pow, div_eq_mul_inv,
        inv_pow (p : ℝ) (k + 2)]

Premises used: zero_le, Ne.symm, inv_pow, div_eq_mul_inv, Nat.cast, _private.0.ArithmeticFunction.vonMangoldt.F₀, _private.0.ArithmeticFunction.vonMangoldt.F'', HAdd.hAdd, Subtype.prop, Nat.Prime.not_prime_pow, Prod.map_apply, reduceIte, Function.comp_apply, Nat.cast_pow, OfNat.ofNat, _private.0.ArithmeticFunction.vonMangoldt.F', Subtype.val, ArithmeticFunction.vonMangoldt_apply_prime, ArithmeticFunction.vonMangoldt_apply_pow, le_add_iff_nonneg_left, id_eq, Nat.zero_ne_add_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
p : Nat.Primes
k : ℕ
⊢ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (1 / 2) / (1 / 2) * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (k + 2) =
    2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (-1 / 2) * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (k + 2)

Tactic:
simp only [← div_mul, div_one, mul_comm, neg_div, Real.inv_rpow p.val.cast_nonneg,
        ← Real.rpow_neg p.val.cast_nonneg, neg_neg]

Premises used: Real.inv_rpow, neg_div, Nat.cast_nonneg, neg_neg, div_mul, mul_comm, Subtype.val, div_one, Real.rpow_neg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
p : Nat.Primes
k : ℕ
⊢ 0 < (↑p : ℕ)

Tactic:
have := p.prop.pos
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
p : Nat.Primes
k : ℕ
this : 0 < (↑p : ℕ)
⊢ LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
p : Nat.Primes
k : ℕ
rw :
  2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ ((↑k : ℝ) + (2 + -1 / 2)) =
    2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ ((↑k : ℝ) + 3 / 2)
⊢ 2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (-1 / 2) * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (k + 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]

Premises used: add_assoc, mul_assoc, add_comm, Nat.cast_add, Real.rpow_add, Nat.cast_two, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
p : Nat.Primes
k : ℕ
⊢ 2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ ((↑k : ℝ) + (2 + -1 / 2)) =
    2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ ((↑k : ℝ) + 3 / 2)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
⊢ ∀ (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)
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)
⊢ Summable F''

Tactic:
(Summable.mul_left 2 this).of_nonneg_of_le (fun pk ↦ ?_) (fun pk ↦ F''_le pk.1 pk.2)

Premises used: Summable.of_nonneg_of_le, Prod.fst, Summable.mul_left, OfNat.ofNat, Prod.snd, _private.0.ArithmeticFunction.vonMangoldt.F''_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 × ℕ
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))
⊢ 0 ≤ F'' pk

Tactic:
simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]

Premises used: Prod.map_snd, _private.0.ArithmeticFunction.vonMangoldt.F₀, _private.0.ArithmeticFunction.vonMangoldt.F'', Prod.map_fst, Function.comp_apply, Nat.cast_pow, _private.0.ArithmeticFunction.vonMangoldt.F', id_eq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 × ℕ
positivity positivity₁ positivity₂ 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))
⊢ 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))]

Premises used: ArithmeticFunction.vonMangoldt_nonneg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
suffices : Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
⊢ Summable F''

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))]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
h : ∀ (pk : Nat.Primes × ℕ), HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)
| Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)

Tactic:
enter [1, pk]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
pk : Nat.Primes × ℕ
h : HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
| HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)

Tactic:
rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]

Premises used: Prod.fst, Real.rpow_add, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
h :
  ∀ (pk : Nat.Primes × ℕ),
    HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
| Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)

Tactic:
enter [1, pk]; rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]

Premises used: Real.rpow_add, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
conv :
  Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦
    HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)
⊢ Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ ((↑pk.2 : ℝ) + 3 / 2)

Tactic:
conv => enter [1, pk]; rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]

Premises used: Real.rpow_add, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
x : Nat.Primes × ℕ
⊢ 0 x ≤ HPow.hPow (α := ℝ) (↑(↑x.1 : ℕ) : ℝ)⁻¹ x.2 * HPow.hPow (α := ℝ) (↑(↑x.1 : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)
refine_2 :
  Summable (α := ℝ) fun (x : Nat.Primes) ↦
    ∑' (y : ℕ),
      HPow.hPow (α := ℝ) (↑(↑(x, y).1 : ℕ) : ℝ)⁻¹ (x, y).2 * HPow.hPow (α := ℝ) (↑(↑(x, y).1 : ℕ) : ℝ)⁻¹ (3 / 2)
⊢ Summable (α := ℝ) fun (pk : Nat.Primes × ℕ) ↦
    HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ pk.2 * HPow.hPow (α := ℝ) (↑(↑pk.1 : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
refine (summable_prod_of_nonneg (fun _ ↦ by positivity)).mpr ⟨(fun p ↦ ?_), ?_⟩

Premises used: Iff.mpr, And.intro, summable_prod_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
refine_1 :
  Summable (α := ℝ) fun (y : ℕ) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
⊢ Summable (α := ℝ) fun (y : ℕ) ↦
    HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (p, y).2 * HPow.hPow (α := ℝ) (↑(↑(p, y).1 : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
dsimp only
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
Summable.mul_right _ <| summable_geometric_of_lt_one (hp₀ p).le (hp₁ p)

Premises used: Summable.mul_right, LT.lt.le, summable_geometric_of_lt_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
exact Summable.mul_right _ <| summable_geometric_of_lt_one (hp₀ p).le (hp₁ p)

Premises used: Summable.mul_right, LT.lt.le, summable_geometric_of_lt_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
h :
  ∀ (p : Nat.Primes), ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
| Summable (α := ℝ) fun (x : Nat.Primes) ↦
    ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
enter [1, p]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
h : (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
| ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]

Premises used: tsum_geometric_of_lt_one, LT.lt.le, tsum_mul_right
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
h : ∀ (p : Nat.Primes), (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
| Summable (α := ℝ) fun (x : Nat.Primes) ↦
    ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
enter [1, p]; rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]

Premises used: tsum_mul_right
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
refine_2 :
  Summable (α := ℝ) fun (p : Nat.Primes) ↦
    (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
⊢ Summable (α := ℝ) fun (x : Nat.Primes) ↦
    ∑' (y : ℕ), HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ y * HPow.hPow (α := ℝ) (↑(↑x : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
conv => enter [1, p]; rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]

Premises used: tsum_mul_right
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
⊢ -(3 / 2) < -1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)
refine_2₁ :
  ∀ (p : Nat.Primes),
    (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2) ≤
      2 * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-(3 / 2))
⊢ Summable (α := ℝ) fun (p : Nat.Primes) ↦
    (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 ↦ ?_)

Premises used: Iff.mpr, Summable.of_nonneg_of_le, Summable.mul_left, Nat.Primes.summable_rpow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  0 < HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹ →
    0 ≤ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)
⊢ 0 ≤ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ (3 / 2)

Tactic:
positivity [sub_pos.mpr (hp₁ p)]

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
refine_2 :
  (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 2))⁻¹ ≤
    2 * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 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]

Premises used: Real.inv_rpow, Nat.cast_nonneg, Subtype.val, Real.rpow_neg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
refine_2 : (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ ≤ 2
⊢ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 2))⁻¹ ≤
    2 * (HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (3 / 2))⁻¹

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ = 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
refine_2 : LE.le (α := ℝ) 2 (↑(↑p : ℕ) : ℝ)
⊢ (HSub.hSub (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)⁻¹)⁻¹ ≤ 2

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]

Premises used: Iff.mpr, sub_pos, inv_le_comm₀, zero_lt_two, le_sub_comm, inv_le_inv₀
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ LE.le (α := ℝ) 2 (↑(↑p : ℕ) : ℝ)

Tactic:
Nat.ofNat_le_cast.mpr p.prop.two_le

Premises used: Iff.mpr, Nat.ofNat_le_cast, Subtype.prop, Nat.Prime.two_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
hp₀ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) 0 (↑(↑p : ℕ) : ℝ)⁻¹
hp₁ : ∀ (p : Nat.Primes), LT.lt (α := ℝ) (↑(↑p : ℕ) : ℝ)⁻¹ 1
p : Nat.Primes
⊢ LE.le (α := ℝ) 2 (↑(↑p : ℕ) : ℝ)

Tactic:
exact Nat.ofNat_le_cast.mpr p.prop.two_le

Premises used: Iff.mpr, Nat.ofNat_le_cast, Subtype.prop, Nat.Prime.two_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
n : ℕ
positivity positivity₁ positivity₂ positivity₃ :
  0 ≤ residueClass a n → 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
⊢ 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)

Tactic:
positivity [residueClass_nonneg a n]

Premises used: ArithmeticFunction.vonMangoldt.residueClass_nonneg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
⊢ ∀ (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]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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

Tactic:
div_le_div_of_nonneg_right ?_ n.cast_nonneg

Premises used: div_le_div_of_nonneg_right, Nat.cast_nonneg, _private.0.ArithmeticFunction.vonMangoldt.F₀
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
n : ℕ
refine : (if Nat.Prime n then 0 else residueClass a n) ≤ if Nat.Prime n then 0 else (Λ : (a : ℕ) → ℝ) n
⊢ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n

Tactic:
refine div_le_div_of_nonneg_right ?_ n.cast_nonneg

Premises used: div_le_div_of_nonneg_right
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
neg : ¬Nat.Prime n → residueClass a n ≤ (Λ : (a : ℕ) → ℝ) n
⊢ (if Nat.Prime n then 0 else residueClass a n) ≤ if Nat.Prime n then 0 else (Λ : (a : ℕ) → ℝ) n

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
n : ℕ
h : Nat.Prime n
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
n : ℕ
h : ¬Nat.Prime n
⊢ residueClass a n ≤ (Λ : (a : ℕ) → ℝ) n

Tactic:
residueClass_le a n

Premises used: ArithmeticFunction.vonMangoldt.residueClass_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)
n : ℕ
h : Nat.Prime n
⊢ LE.le (α := ℝ) 0 0

Tactic:
exacts [le_rfl, residueClass_le a n]

Premises used: le_rfl, ArithmeticFunction.vonMangoldt.residueClass_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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

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]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℝ)

Tactic:
Summable.of_nonneg_of_le h₀ hleF₀ ?_

Premises used: Summable.of_nonneg_of_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
refine : Summable F₀
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ)

Tactic:
refine Summable.of_nonneg_of_le h₀ hleF₀ ?_

Premises used: Summable.of_nonneg_of_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
p : Nat.Primes
⊢ F₀ (↑p : ℕ) = 0

Tactic:
simp only [p.prop, ↓reduceIte, zero_div, F₀]

Premises used: zero_div, _private.0.ArithmeticFunction.vonMangoldt.F₀, Subtype.prop, reduceIte
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ ∀ (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₀]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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₀

Tactic:
(summable_subtype_iff_indicator (s := {n | IsPrimePow n}).mp ?_).congr
      fun n ↦ Set.indicator_apply_eq_self.mpr fun (hn : ¬ IsPrimePow n) ↦ ?_

Premises used: Iff.mpr, Set.indicator_apply_eq_self, Iff.mp, summable_subtype_iff_indicator, Summable.congr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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))
refine_2 : ∀ (n : ℕ) (hn : ¬IsPrimePow n), F₀ n = 0
⊢ Summable F₀

Tactic:
refine (summable_subtype_iff_indicator (s := {n | IsPrimePow n}).mp ?_).congr
      fun n ↦ Set.indicator_apply_eq_self.mpr fun (hn : ¬ IsPrimePow n) ↦ ?_

Premises used: Iff.mpr, Set.indicator_apply_eq_self, Iff.mp, summable_subtype_iff_indicator, Summable.congr