Theorem: SelbergSieve.selberg_bound_weights (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
d : ℕ
⊢ |s.selbergWeights d| ≤ 1
Tactic:
by_cases hdP : d ∣ P
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Tactic:
swap
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Tactic:
have : 1*S ≥ γ d * ↑(μ d) * S := by
  rw[one_mul]
  exact s.selbergBoundingSum_ge hdP
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ |s.selbergWeights d| ≤ 1

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ |s.selbergWeights d| ≤ 1
Tactic:
replace this : γ d * μ d ≤ 1 := by
  apply le_of_mul_le_mul_of_pos_right this (s.selbergBoundingSum_pos)
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| ≤ 1

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| ≤ 1
Tactic:
convert this using 1
State after:
case h.e'_3
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| = s.selbergWeights d * ↑(μ d)

State before:
case h.e'_3
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| = s.selbergWeights d * ↑(μ d)
Tactic:
rw [← abs_of_nonneg <| s.selbergWeights_mul_mu_nonneg d hdP,
  abs_mul, ←Int.cast_abs, abs_moebius_eq_one_of_squarefree <|
  (s.prodPrimes_squarefree.squarefree_of_dvd hdP), Int.cast_one, mul_one]
State after:
no goals

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Tactic:
rw [s.selbergWeights_eq_zero_of_not_dvd hdP]
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |0| ≤ 1

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |0| ≤ 1
Tactic:
simp only [zero_le_one, abs_zero]
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
Tactic:
rw[one_mul]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≥ s.selbergWeights d * ↑(μ d) * S

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≥ s.selbergWeights d * ↑(μ d) * S
Tactic:
exact s.selbergBoundingSum_ge hdP
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ s.selbergWeights d * ↑(μ d) ≤ 1
Tactic:
apply le_of_mul_le_mul_of_pos_right this (s.selbergBoundingSum_pos)
State after:
no goals