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

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ d ∈ P.divisors, ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply sum_congr rfl
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ x then ν x * s.selbergWeights x else 0) =
      ∑ k ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ x then ν x * s.selbergWeights x else 0) =
      ∑ k ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Tactic:
intro d _
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
rw [selbergWeights_eq_dvds_sum, ← boole_mul, mul_sum, mul_sum]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∑ i ∈ P.divisors, (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∑ i ∈ P.divisors, (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply sum_congr rfl
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) =
      if l ∣ d ∧ d ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ d) else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) =
      if l ∣ d ∧ d ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ d) else 0
Tactic:
intro k _
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ k ∧ ↑k ^ 2 ≤ y then g k else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ k ∧ ↑k ^ 2 ≤ y then g k else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
rw [mul_ite_zero, ite_zero_mul_ite_zero]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then 1 * (S⁻¹ * ↑(μ d) * g k) else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then 1 * (S⁻¹ * ↑(μ d) * g k) else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply if_ctx_congr Iff.rfl _ (fun _ => rfl)
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)
Tactic:
intro _
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝² : d ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝² : d ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)
Tactic:
ring
State after:
no goals

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ d ∈ P.divisors, ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Tactic:
rw [sum_comm]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ y ∈ P.divisors, ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ y ∧ ↑y ^ 2 ≤ y then g y * S⁻¹ * ↑(μ x) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ y ∈ P.divisors, ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ y ∧ ↑y ^ 2 ≤ y then g y * S⁻¹ * ↑(μ x) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Tactic:
apply sum_congr rfl
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if l ∣ x_1 ∧ x_1 ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ x_1) else 0) =
      if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if l ∣ x_1 ∧ x_1 ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ x_1) else 0) =
      if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0
Tactic:
intro k _
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0) =
    if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0) =
    if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Tactic:
apply symm
State after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0

State before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Tactic:
rw [← boole_mul, sum_mul, sum_mul, mul_sum, sum_congr rfl]
State after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ x ∧ x ∣ k then ↑(μ x) else 0) * g k * S⁻¹) =
      if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0

State before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ x ∧ x ∣ k then ↑(μ x) else 0) * g k * S⁻¹) =
      if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Tactic:
intro d _
State after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0

State before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
rw [ite_zero_mul, ite_zero_mul, ite_zero_mul, one_mul, ←ite_and]
State after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k then ↑(μ d) * g k * S⁻¹ else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0

State before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k then ↑(μ d) * g k * S⁻¹ else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply if_ctx_congr _ _ (fun _ => rfl)
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k ↔ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)
Tactic:
intro _
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝² : k ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝² : k ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)
Tactic:
ring
State after:
no goals

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k ↔ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
Tactic:
tauto
State after:
no goals

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0
Tactic:
rw [Aux.sum_intro (f:=fun _ => if l^2 ≤ y then g l * μ l * S⁻¹ else 0) (divisors P) l hl]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ k ∈ P.divisors, if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ k ∈ P.divisors, if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Tactic:
apply sum_congr rfl
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0) =
      if x = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0) =
      if x = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Tactic:
intro k hk
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Tactic:
rw [Aux.moebius_inv_dvd_lower_bound_real s.prodPrimes_squarefree l _ (dvd_of_mem_divisors hk),
  ←ite_and, ite_zero_mul, ite_zero_mul, ← ite_and]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l = k then ↑(μ l) * g k * S⁻¹ else 0) = if k = l ∧ ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l = k then ↑(μ l) * g k * S⁻¹ else 0) = if k = l ∧ ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0
Tactic:
apply if_ctx_congr _ _ fun _ => rfl
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l = k ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l = k ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
rw [and_comm, eq_comm]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑k ^ 2 ≤ y ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑k ^ 2 ≤ y ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
apply and_congr_right
State after:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l → (↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y)

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹

State before:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l → (↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y)

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
intro heq
State after:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
heq : k = l
⊢ ↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹

State before:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
heq : k = l
⊢ ↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
rw [heq]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
intro h
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
rw[h.1]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g l * S⁻¹ = g l * ↑(μ l) * S⁻¹

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g l * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
ring
State after:
no goals