-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The function `n ↦ Λ n / n`, restricted to non-primes in a residue class, is summable.
This is used to convert results on `ArithmeticFunction.vonMangoldt.residueClass` to results
on primes in an arithmetic progression. -/
lemma summable_residueClass_non_primes_div :
    Summable fun n : ℕ ↦ (if n.Prime then 0 else residueClass a n) / n

Proof state:
q : ℕ
a : ZMod q
n : ℕ
⊢ 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n

Tactic:
have := residueClass_nonneg a n

Result:
q : ℕ
a : ZMod q
n : ℕ
this : 0 ≤ residueClass a n
⊢ 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n

Proof state:
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
⊢ Summable ArithmeticFunction.vonMangoldt.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) ↦ ?_

Result:
case refine_1
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
⊢ Summable (ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val)

case refine_2
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
n : ℕ
hn : ¬IsPrimePow n
⊢ ArithmeticFunction.vonMangoldt.F₀ n = 0

Proof state:
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
⊢ Summable ArithmeticFunction.vonMangoldt.F₀

Tactic:
have hF₀ (p : Nat.Primes) : F₀ p.val = 0 := by
  simp only [p.prop, ↓reduceIte, zero_div, F₀]

Result:
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
⊢ Summable ArithmeticFunction.vonMangoldt.F₀

Proof state:
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
⊢ ArithmeticFunction.vonMangoldt.F'' = ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1

Tactic:
ext1

Result:
case h
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
x✝ : Nat.Primes × ℕ
⊢ ArithmeticFunction.vonMangoldt.F'' x✝ = (ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1) x✝

Proof state:
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
⊢ (ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val) ∘ ⇑prodNatEquiv = ArithmeticFunction.vonMangoldt.F'

Tactic:
ext1 n

Result:
case h
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
n : Nat.Primes × ℕ
⊢ ((ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val) ∘ ⇑prodNatEquiv) n = ArithmeticFunction.vonMangoldt.F' n

Proof state:
case refine_1
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
hF'₁ : ArithmeticFunction.vonMangoldt.F'' = ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1
⊢ Summable ArithmeticFunction.vonMangoldt.F'

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

Result:
case refine_1.refine_1
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
hF'₁ : ArithmeticFunction.vonMangoldt.F'' = ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1
⊢ Function.Injective (Prod.map _root_.id fun x => x + 1)

case refine_1.refine_2
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
hFF' : ArithmeticFunction.vonMangoldt.F₀ ∘ Subtype.val = ArithmeticFunction.vonMangoldt.F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F' (p, 0) = 0
hF'₁ : ArithmeticFunction.vonMangoldt.F'' = ArithmeticFunction.vonMangoldt.F' ∘ Prod.map _root_.id fun x => x + 1
u : Nat.Primes × ℕ
hu : u ∉ Set.range (Prod.map _root_.id fun x => x + 1)
⊢ ArithmeticFunction.vonMangoldt.F' u = 0

Proof state:
case h
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 ≤ ArithmeticFunction.vonMangoldt.F₀ n
hF₀ : ∀ (p : Nat.Primes), ArithmeticFunction.vonMangoldt.F₀ ↑p = 0
n : Nat.Primes × ℕ
⊢ ArithmeticFunction.vonMangoldt.F₀ ↑(prodNatEquiv n) = ArithmeticFunction.vonMangoldt.F₀ (↑n.1 ^ (n.2 + 1))

Tactic:
congr

Result:
no goals