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

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * w d2 = 0
Tactic:
rw [hw d2]
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * 0 = 0

s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * 0 = 0

s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y
Tactic:
ring
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y
Tactic:
by_contra hyp
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ False

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ False
Tactic:
apply hd
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ y

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ y
Tactic:
apply le_trans _ hyp
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ ↑d2 ^ 2

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ ↑d2 ^ 2
Tactic:
norm_cast
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d ≤ d2 ^ 2

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d ≤ d2 ^ 2
Tactic:
calc _ ≤ (d1.lcm d2) := by rw [h]
    _ ≤ (d1*d2) := Nat.div_le_self _ _
    _ ≤ _       := ?_
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 ^ 2

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d ≤ d1.lcm d2
Tactic:
rw [h]
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 ^ 2
Tactic:
rw [sq]
State after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 * d2

State before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 * d2
Tactic:
gcongr
State after:
no goals