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

State before:
n p : ℕ
hp : p.Prime
⊢ p ∣ primorial n ↔ p ≤ n
Tactic:
unfold primorial
State after:
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ↔ p ≤ n

State before:
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ↔ p ≤ n
Tactic:
constructor
State after:
case mp
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p → p ≤ n

case mpr
n p : ℕ
hp : p.Prime
⊢ p ≤ n → p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p

State before:
case mp
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p → p ≤ n
Tactic:
intro h
State after:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
⊢ p ≤ n

State before:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
⊢ p ≤ n
Tactic:
let h' : ∃ i, i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
State after:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
⊢ p ≤ n

State before:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
⊢ p ≤ n
Tactic:
cases' h' with q hq
State after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : q ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ q
⊢ p ≤ n

State before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : q ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ q
⊢ p ≤ n
Tactic:
rw [Finset.mem_filter, Finset.mem_range] at hq
State after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p ∣ q
⊢ p ≤ n

State before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p ∣ q
⊢ p ≤ n
Tactic:
rw [prime_dvd_prime_iff_eq (Nat.Prime.prime hp) (Nat.Prime.prime hq.1.2)] at hq
State after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ p ≤ n

State before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ p ≤ n
Tactic:
rw [hq.2]
State after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ q ≤ n

State before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ q ≤ n
Tactic:
exact Nat.lt_succ.mp hq.1.1
State after:
no goals

State before:
case mpr
n p : ℕ
hp : p.Prime
⊢ p ≤ n → p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
Tactic:
intro h
State after:
case mpr
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p

State before:
case mpr
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
Tactic:
apply Finset.dvd_prod_of_mem
State after:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))

State before:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))
Tactic:
rw [Finset.mem_filter, Finset.mem_range]
State after:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p < n + 1 ∧ p.Prime

State before:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p < n + 1 ∧ p.Prime
Tactic:
exact ⟨Nat.lt_succ.mpr h, hp⟩
State after:
no goals