Theorem: Sieve.primorial_squarefree (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
n : ℕ
⊢ Squarefree (primorial n)
Tactic:
apply prodDistinctPrimes_squarefree
State after:
case h
n : ℕ
⊢ ∀ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p.Prime

State before:
case h
n : ℕ
⊢ ∀ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p.Prime
Tactic:
simp_rw [Finset.mem_filter]
State after:
case h
n : ℕ
⊢ ∀ (p : ℕ), p ∈ Finset.range (n + 1) ∧ p.Prime → p.Prime

State before:
case h
n : ℕ
⊢ ∀ (p : ℕ), p ∈ Finset.range (n + 1) ∧ p.Prime → p.Prime
Tactic:
exact fun _ h => h.2
State after:
no goals