awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
hn : ¬IsPrimePow n
⊢ F₀ n = 0

Tactic:
simp +contextual only [div_eq_zero_iff, ite_eq_left_iff, vonMangoldt_eq_zero_iff, hn,
      not_false_eq_true, implies_true, Nat.cast_eq_zero, true_or, F₀]

Premises used: ite_eq_left_iff, true_or, _private.0.ArithmeticFunction.vonMangoldt.F₀, Nat.cast_eq_zero, ArithmeticFunction.vonMangoldt_eq_zero_iff, implies_true, not_false_eq_true, div_eq_zero_iff
-- 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
⊢ Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))

Tactic:
(Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_

Premises used: Iff.mpr, Set.Mem, IsPrimePow, setOf, Function.comp, Equiv.eq_comp_symm, _private.0.ArithmeticFunction.vonMangoldt.F₀, Nat.Primes.prodNatEquiv, _private.0.ArithmeticFunction.vonMangoldt.F', Subtype.val
-- 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 :
  Function.comp (β := { n : ℕ // IsPrimePow n }) (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ IsPrimePow n))
      (⇑prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) =
    F'
⊢ Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))

Tactic:
refine (Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_

Premises used: Iff.mpr, Function.comp, Equiv.eq_comp_symm, _private.0.ArithmeticFunction.vonMangoldt.F₀, Nat.Primes.prodNatEquiv, _private.0.ArithmeticFunction.vonMangoldt.F', Subtype.val
-- 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
h :
  ∀ (n : Nat.Primes × ℕ),
    Function.comp (β := { n : ℕ // IsPrimePow n }) (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ IsPrimePow n))
        (⇑prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) n =
      F' n
⊢ Function.comp (β := { n : ℕ // IsPrimePow n }) (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ IsPrimePow n))
      (⇑prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) =
    F'

Tactic:
ext1 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
hF₀ : ∀ (p : Nat.Primes), F₀ (↑p : ℕ) = 0
n : Nat.Primes × ℕ
⊢ F₀ (↑((prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) n) : ℕ) = F₀ ((↑n.1 : ℕ) ^ (n.2 + 1))

Tactic:
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
⊢ Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))

Tactic:
have hFF' :
      F₀ ∘ Subtype.val (p := fun n ↦ n ∈ {n | IsPrimePow n}) = F' ∘ ⇑prodNatEquiv.symm := by
    refine (Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_
    ext1 n
    simp only [Function.comp_apply, F']
    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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
refine_1 :
  Summable (β := (↑{n : ℕ | IsPrimePow n} : Type))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
⊢ Summable (β := (↑{n : ℕ | IsPrimePow n} : Type))
    (F₀ ∘ Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} x))

Tactic:
rw [hFF']
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
⊢ Summable (β := (↑{n : ℕ | IsPrimePow n} : Type))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))

Tactic:
(Nat.Primes.prodNatEquiv.symm.summable_iff (f := F')).mpr ?_

Premises used: Iff.mpr, Set.Mem, IsPrimePow, setOf, Equiv.summable_iff, Nat.Primes.prodNatEquiv, Equiv.symm
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
refine_1 : Summable F'
⊢ Summable (β := (↑{n : ℕ | IsPrimePow n} : Type))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))

Tactic:
refine (Nat.Primes.prodNatEquiv.symm.summable_iff (f := F')).mpr ?_

Premises used: Iff.mpr, Equiv.summable_iff, Nat.Primes.prodNatEquiv, Equiv.symm
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
p : Nat.Primes
⊢ F' (p, 0) = 0

Tactic:
simp only [zero_add, pow_one, hF₀, F']

Premises used: zero_add, pow_one, _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 : ℝ)
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ (↑p : ℕ) = 0
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
⊢ ∀ (p : Nat.Primes), F' (p, 0) = 0

Tactic:
have hF'₀ (p : Nat.Primes) : F' (p, 0) = 0 := by simp only [zero_add, pow_one, hF₀, 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
h : ∀ (x : Nat.Primes × ℕ), F'' x = (F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1) x
⊢ F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1

Tactic:
ext1
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
x : Nat.Primes × ℕ
⊢ F'' x = (F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1) x

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

Premises used: Prod.map_snd, _private.0.ArithmeticFunction.vonMangoldt.F'', Prod.map_fst, Function.comp_apply, _private.0.ArithmeticFunction.vonMangoldt.F', id_eq
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
⊢ F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1

Tactic:
have hF'₁ : F'' = F' ∘ (Prod.map _root_.id (· + 1)) := by
    ext1
    simp only [Function.comp_apply, Prod.map_fst, id_eq, Prod.map_snd, F'', 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1
⊢ Summable F'

Tactic:
(Function.Injective.summable_iff ?_ fun u hu ↦ ?_).mp <| hF'₁ ▸ summable_F''

Premises used: Function.Injective.summable_iff, Iff.mp
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1
refine_1 : Function.Injective (α := Nat.Primes × ℕ) (β := Nat.Primes × ℕ) (Prod.map id fun (x : ℕ) ↦ x + 1)
refine_1₁ :
  ∀ (u : Nat.Primes × ℕ) (hu : u ∉ Set.range (ι := Nat.Primes × ℕ) (Prod.map id fun (x : ℕ) ↦ x + 1)), F' u = 0
⊢ Summable F'

Tactic:
refine (Function.Injective.summable_iff ?_ fun u hu ↦ ?_).mp <| hF'₁ ▸ summable_F''

Premises used: Function.Injective.summable_iff, Iff.mp
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1
⊢ Function.Injective (α := Nat.Primes × ℕ) (β := Nat.Primes × ℕ) (Prod.map id fun (x : ℕ) ↦ x + 1)

Tactic:
Function.Injective.prodMap (fun ⦃a₁ a₂⦄ a ↦ a) <| add_left_injective 1

Premises used: Function.Injective.prodMap, add_left_injective, OfNat.ofNat
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1
⊢ Function.Injective (α := Nat.Primes × ℕ) (β := Nat.Primes × ℕ) (Prod.map id fun (x : ℕ) ↦ x + 1)

Tactic:
exact Function.Injective.prodMap (fun ⦃a₁ a₂⦄ a ↦ a) <| add_left_injective 1

Premises used: Function.Injective.prodMap, add_left_injective, OfNat.ofNat
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1
u : Nat.Primes × ℕ
hu : u ∉ Set.range (ι := Nat.Primes × ℕ) (Prod.map id fun (x : ℕ) ↦ x + 1)
⊢ u.2 = 0

Tactic:
simp only [Set.range_prodMap, Set.range_id, Set.mem_prod, Set.mem_univ, Set.mem_range,
      Nat.exists_add_one_eq, true_and, not_lt, nonpos_iff_eq_zero] at hu

Premises used: Set.mem_range, Set.range_prodMap, Set.mem_prod, not_lt, Nat.exists_add_one_eq, Set.range_id, Set.mem_univ, true_and, nonpos_iff_eq_zero
-- 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
hFF' :
  Eq (α := { n : ℕ // Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n } → ℝ)
    (F₀ ∘ Subtype.val (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n : ℕ | IsPrimePow n} n))
    (F' ∘ (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun (x : ℕ) ↦ x + 1
u : Nat.Primes × ℕ
hu : u.2 = 0
refine_1 : F' u = F' (u.1, 0)
refine_1₁ refine_1₂ : F' u = F' (u.1, u.2)
⊢ F' u = 0

Tactic:
rw [← hF'₀ u.1, ← hu]

Premises used: Prod.fst
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
n : ℕ
rw :
  (↑q.totient : ℂ) * (↑(residueClass a n) : ℂ) =
    ∑ χ : DirichletCharacter ℂ q,
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) ((χ : (a : ZMod q) → ℂ) (↑n : ZMod q) : ℂ) *
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)
⊢ (↑(residueClass a n) : ℂ) =
    HMul.hMul (α := ℂ) (↑q.totient : ℂ)⁻¹
      (∑ χ : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) ((χ : (a : ZMod q) → ℂ) (↑n : ZMod q) : ℂ) *
          (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))

Tactic:
rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']

Premises used: Iff.mpr, eq_inv_mul_iff_mul_eq₀, LT.lt.ne', Nat.pos_of_neZero, Nat.totient_pos
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
n : ℕ
⊢ (↑q.totient : ℂ) * (↑(residueClass a n) : ℂ) =
    ∑ χ : DirichletCharacter ℂ q,
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) ((χ : (a : ZMod q) → ℂ) (↑n : ZMod q) : ℂ) *
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)

Tactic:
simp +contextual only [residueClass, Set.indicator_apply, Set.mem_setOf_eq, apply_ite,
    ofReal_zero, mul_zero, ← Finset.sum_mul, sum_char_inv_mul_char_eq ℂ ha n, eq_comm (a := a),
    ite_mul, zero_mul, ↓reduceIte, ite_self]

Premises used: Set.indicator_apply, ite_self, MulZeroClass.zero_mul, apply_ite, DirichletCharacter.sum_char_inv_mul_char_eq, Set.mem_setOf_eq, eq_comm, ArithmeticFunction.vonMangoldt.residueClass, Nat.cast, MulZeroClass.mul_zero, Complex.ofReal_zero, ite_mul, reduceIte, Complex, Finset.sum_mul
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
h :
  ∀ (n : ℕ),
    (↑(residueClass a n) : ℂ) =
      HSMul.hSMul (α := ℂ) (β := (n : ℕ) → ℂ) (↑q.totient : ℂ)⁻¹
        (∑ χ : DirichletCharacter ℂ q,
          HSMul.hSMul (α := ℂ) (β := (n : ℕ) → ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) fun (n : ℕ) ↦
            HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) (↑n : ZMod q) : ℂ) (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
        n
⊢ (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) =
    HSMul.hSMul (α := ℂ) (β := (n : ℕ) → ℂ) (↑q.totient : ℂ)⁻¹
      (∑ χ : DirichletCharacter ℂ q,
        HSMul.hSMul (α := ℂ) (β := (n : ℕ) → ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) fun (n : ℕ) ↦
          HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) (↑n : ZMod q) : ℂ) (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
n : ℕ
⊢ (↑(residueClass a n) : ℂ) =
    HSMul.hSMul (α := ℂ) (β := (n : ℕ) → ℂ) (↑q.totient : ℂ)⁻¹
      (∑ χ : DirichletCharacter ℂ q,
        HSMul.hSMul (α := ℂ) (β := (n : ℕ) → ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) fun (n : ℕ) ↦
          HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) (↑n : ZMod q) : ℂ) (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
      n

Tactic:
simpa only [Pi.smul_apply, Finset.sum_apply, smul_eq_mul, ← mul_assoc]
    using residueClass_apply ha n

Premises used: mul_assoc, ArithmeticFunction.vonMangoldt.residueClass_apply, Finset.sum_apply, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
simp :
  L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    HMul.hMul (α := ℂ) (↑q.totient : ℂ)⁻¹
      (∑ x : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
          (L
            (HMul.hMul (α := ℕ → ℂ) (fun (x_1 : ℕ) ↦ (x : (a : ZMod q) → ℂ) (↑x_1 : ZMod q)) fun (n : ℕ) ↦
              (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
            s))
⊢ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    HMul.hMul (α := ℂ) (-(↑q.totient : ℂ)⁻¹)
      (∑ χ : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s / LFunction χ s))

Tactic:
simp only [deriv_LFunction_eq_deriv_LSeries _ hs, LFunction_eq_LSeries _ hs, neg_mul, ← mul_neg,
    ← Finset.sum_neg_distrib, ← neg_div, ← LSeries_twist_vonMangoldt_eq _ hs]

Premises used: neg_div, DirichletCharacter.LSeries_twist_vonMangoldt_eq, DirichletCharacter.LFunction_eq_LSeries, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, neg_mul, Finset.sum_neg_distrib, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
rw :
  (↑q.totient : ℂ) * L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    ∑ x : DirichletCharacter ℂ q,
      HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
        (L
          (HMul.hMul (α := ℕ → ℂ) (fun (x_1 : ℕ) ↦ (x : (a : ZMod q) → ℂ) (↑x_1 : ZMod q)) fun (n : ℕ) ↦
            (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
          s)
⊢ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    HMul.hMul (α := ℂ) (↑q.totient : ℂ)⁻¹
      (∑ x : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
          (L
            (HMul.hMul (α := ℕ → ℂ) (fun (x_1 : ℕ) ↦ (x : (a : ZMod q) → ℂ) (↑x_1 : ZMod q)) fun (n : ℕ) ↦
              (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
            s))

Tactic:
rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']

Premises used: Iff.mpr, eq_inv_mul_iff_mul_eq₀, LT.lt.ne', Nat.pos_of_neZero, Nat.totient_pos
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
simp_rw :
  L (HSMul.hSMul (α := ℂ) (β := ℕ → ℂ) (↑q.totient : ℂ) fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    L
      (∑ i : DirichletCharacter ℂ q,
        HSMul.hSMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
          (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (i : (a : ZMod q) → ℂ) (↑n : ZMod q)) fun (n : ℕ) ↦
            (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)))
      s
⊢ (↑q.totient : ℂ) * L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    ∑ x : DirichletCharacter ℂ q,
      HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
        (L
          (HMul.hMul (α := ℕ → ℂ) (fun (x_1 : ℕ) ↦ (x : (a : ZMod q) → ℂ) (↑x_1 : ZMod q)) fun (n : ℕ) ↦
            (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
          s)

Tactic:
simp_rw [← LSeries_smul,
    ← LSeries_sum <| fun χ _ ↦ (LSeriesSummable_twist_vonMangoldt χ hs).smul _]

Premises used: LSeriesSummable.smul, LSeries_smul, DirichletCharacter.LSeriesSummable_twist_vonMangoldt, LSeries_sum
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (HSMul.hSMul (α := ℂ) (β := ℕ → ℂ) (↑q.totient : ℂ) fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    L
      (∑ i : DirichletCharacter ℂ q,
        HSMul.hSMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
          (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (i : (a : ZMod q) → ℂ) (↑n : ZMod q)) fun (n : ℕ) ↦
            (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)))
      s

Tactic:
LSeries_congr (fun {n} _ ↦ ?_) s

Premises used: LSeries_congr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
refine :
  ∀ {n : ℕ},
    n ≠ 0 →
      HSMul.hSMul (α := ℂ) (β := ℕ → ℂ) (↑q.totient : ℂ) (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) n =
        (∑ i : DirichletCharacter ℂ q,
            HSMul.hSMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
              (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (i : (a : ZMod q) → ℂ) (↑n : ZMod q)) fun (n : ℕ) ↦
                (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)))
          n
⊢ L (HSMul.hSMul (α := ℂ) (β := ℕ → ℂ) (↑q.totient : ℂ) fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s =
    L
      (∑ i : DirichletCharacter ℂ q,
        HSMul.hSMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
          (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (i : (a : ZMod q) → ℂ) (↑n : ZMod q)) fun (n : ℕ) ↦
            (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)))
      s

Tactic:
refine LSeries_congr (fun {n} _ ↦ ?_) s

Premises used: LSeries_congr