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

State before:
s : Sieve
d : ℕ
hd : d ∈ P.divisors
⊢ Squarefree d
Tactic:
simp only [Nat.mem_divisors] at hd
State after:
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ Squarefree d

State before:
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ Squarefree d
Tactic:
exact Squarefree.squarefree_of_dvd hd.left s.prodPrimes_squarefree
State after:
no goals