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

State before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
⊢ ν d < 1
Tactic:
have hd_sq : Squarefree d := Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree
State after:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ν d < 1

State before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∏ p ∈ d.primeFactors, ν p < ∏ p ∈ d.primeFactors, 1
Tactic:
apply prod_lt_prod_of_nonempty
State after:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, 0 < ν i

case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, ν i < 1

case h_ne
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ d.primeFactors.Nonempty

State before:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, 0 < ν i
Tactic:
intro p hp
State after:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p ∈ d.primeFactors
⊢ 0 < ν p

State before:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p ∈ d.primeFactors
⊢ 0 < ν p
Tactic:
simp only [mem_primeFactors] at hp
State after:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p.Prime ∧ p ∣ d ∧ d ≠ 0
⊢ 0 < ν p

State before:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p.Prime ∧ p ∣ d ∧ d ≠ 0
⊢ 0 < ν p
Tactic:
apply s.nu_pos_of_prime p (by aesop) (hp.2.1.trans hdP)
State after:
no goals

State before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p.Prime ∧ p ∣ d ∧ d ≠ 0
⊢ p.Prime
Tactic:
aesop
State after:
no goals

State before:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, ν i < 1
Tactic:
intro p hpd
State after:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p ∈ d.primeFactors
⊢ ν p < 1

State before:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p ∈ d.primeFactors
⊢ ν p < 1
Tactic:
rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
State after:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p.Prime ∧ p ∣ d
⊢ ν p < 1

State before:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p.Prime ∧ p ∣ d
⊢ ν p < 1
Tactic:
apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
State after:
no goals

State before:
case h_ne
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ d.primeFactors.Nonempty
Tactic:
apply primeDivisors_nonempty _ <| (two_le_iff d).mpr ⟨hd_sq.ne_zero, hd_ne_one⟩
State after:
no goals

State before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∏ p ∈ d.primeFactors, 1 = 1
Tactic:
simp
State after:
no goals