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

State before:
s : SelbergSieve
⊢ s.selbergWeights 1 = 1
Tactic:
dsimp only [selbergWeights]
State after:
s : SelbergSieve
⊢ (if 1 ∣ P then (ν 1)⁻¹ * g 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0
    else 0) =
    1

State before:
s : SelbergSieve
⊢ (if 1 ∣ P then (ν 1)⁻¹ * g 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0
    else 0) =
    1
Tactic:
rw [if_pos (one_dvd P), s.nu_mult.left, s.selbergTerms_mult.left]
State after:
s : SelbergSieve
⊢ (1⁻¹ * 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0) = 1

State before:
s : SelbergSieve
⊢ (1⁻¹ * 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0) = 1
Tactic:
simp only [inv_one, mul_one, isUnit_one, IsUnit.squarefree, moebius_apply_of_squarefree,
  cardFactors_one, _root_.pow_zero, Int.cast_one, selbergBoundingSum, cast_pow, one_mul,
  coprime_one_right_eq_true, and_true, cast_one]
State after:
s : SelbergSieve
⊢ ((∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ * ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) = 1

State before:
s : SelbergSieve
⊢ ((∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ * ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) = 1
Tactic:
rw [inv_mul_cancel]
State after:
s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) ≠ 0

State before:
s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) ≠ 0
Tactic:
convert s.selbergBoundingSum_ne_zero
State after:
no goals