Theorem: Sieve.lambdaSquared_eq_zero_of_support (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean)

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
⊢ lambdaSquared w d = 0
Tactic:
dsimp only [lambdaSquared]
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
by_cases hy : 0 ≤ y
State after:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
swap
State after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
State after:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0

State before:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0
Tactic:
intro d1 _
State after:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
State after:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0

State before:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0
Tactic:
intro d2 _
State after:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
split_ifs with h
State after:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0

State before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0
Tactic:
swap
State after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0

case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0

State before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0

case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0
Tactic:
rfl
State after:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0

State before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0
Tactic:
rcases Nat.le_or_le d1 d2 with hle | hle
State after:
case pos.inl
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * w d2 = 0

case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d1 * w d2 = 0

State before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
push_neg at hd hy
State after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
have : ∀ d' : ℕ, w d' = 0 := by
  intro d'; apply hw
  have : (0:ℝ) ≤ (d') ^ 2 := by norm_num
  linarith
State after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
State after:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0

State before:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0
Tactic:
intro d1 _
State after:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
State after:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0

State before:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0
Tactic:
intro d2 _
State after:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

State before:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
rw [this d1, this d2]
State after:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then 0 * 0 else 0) = 0

State before:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then 0 * 0 else 0) = 0
Tactic:
simp only [ite_self, eq_self_iff_true, MulZeroClass.mul_zero]
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
⊢ ∀ (d' : ℕ), w d' = 0
Tactic:
intro d'
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ w d' = 0

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ w d' = 0
Tactic:
apply hw
State after:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ ¬↑d' ^ 2 ≤ y

State before:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ ¬↑d' ^ 2 ≤ y
Tactic:
have : (0:ℝ) ≤ (d') ^ 2 := by norm_num
State after:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
this : 0 ≤ ↑d' ^ 2
⊢ ¬↑d' ^ 2 ≤ y

State before:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
this : 0 ≤ ↑d' ^ 2
⊢ ¬↑d' ^ 2 ≤ y
Tactic:
linarith
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ 0 ≤ ↑d' ^ 2
Tactic:
norm_num
State after:
no goals

State before:
case pos.inl
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * w d2 = 0
Tactic:
apply lambdaSquared_eq_zero_of_support_wlog hw hd d1 d2 h hle
State after:
no goals

State before:
case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d1 * w d2 = 0
Tactic:
rw[mul_comm]
State after:
case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d2 * w d1 = 0

State before:
case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d2 * w d1 = 0
Tactic:
apply lambdaSquared_eq_zero_of_support_wlog hw hd d2 d1 (Nat.lcm_comm d1 d2 ▸ h) hle
State after:
no goals