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

State before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
⊢ Squarefree (∏ p ∈ s, p)
Tactic:
refine Iff.mpr Nat.squarefree_iff_prime_squarefree ?_
State after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
⊢ ∀ (x : ℕ), x.Prime → ¬x * x ∣ ∏ p ∈ s, p

State before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
⊢ ∀ (x : ℕ), x.Prime → ¬x * x ∣ ∏ p ∈ s, p
Tactic:
intro p hp
State after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
⊢ ¬p * p ∣ ∏ p ∈ s, p

State before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
⊢ ¬p * p ∣ ∏ p ∈ s, p
Tactic:
by_contra h_dvd
State after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
⊢ False

State before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
⊢ False
Tactic:
by_cases hps : p ∈ s
State after:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∈ s
⊢ False

case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
⊢ False

State before:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∈ s
⊢ False
Tactic:
rw [←Finset.mul_prod_erase (a:=p) (h := hps), mul_dvd_mul_iff_left (Nat.Prime.ne_zero hp)] at h_dvd
State after:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
⊢ False

State before:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
⊢ False
Tactic:
cases' Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h_dvd with q hq
State after:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : q ∈ s.erase p ∧ p ∣ q
⊢ False

State before:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : q ∈ s.erase p ∧ p ∣ q
⊢ False
Tactic:
rw [Finset.mem_erase] at hq
State after:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : (q ≠ p ∧ q ∈ s) ∧ p ∣ q
⊢ False

State before:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : (q ≠ p ∧ q ∈ s) ∧ p ∣ q
⊢ False
Tactic:
exact hq.1.1 $ symm $ (Nat.prime_dvd_prime_iff_eq hp (h q hq.1.2)).mp hq.2
State after:
no goals

State before:
case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
⊢ False
Tactic:
have : p ∣ ∏ p in s, p := Trans.trans (dvd_mul_right p p) h_dvd
State after:
case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
⊢ False

State before:
case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
⊢ False
Tactic:
cases' Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) this with q hq
State after:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ False

State before:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ False
Tactic:
have heq : p = q := by
  rw [←Nat.prime_dvd_prime_iff_eq hp (h q hq.1)]
  exact hq.2
State after:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False

State before:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False
Tactic:
rw [heq] at hps
State after:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
this : p ∣ ∏ p ∈ s, p
q : ℕ
hps : q ∉ s
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False

State before:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
this : p ∣ ∏ p ∈ s, p
q : ℕ
hps : q ∉ s
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False
Tactic:
exact hps hq.1
State after:
no goals

State before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ p = q
Tactic:
rw [←Nat.prime_dvd_prime_iff_eq hp (h q hq.1)]
State after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ p ∣ q

State before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ p ∣ q
Tactic:
exact hq.2
State after:
no goals