Theorem: prodPrimesIocLeChoose (FromTheBook/Ch02/Bertrand/ProdPrimes.lean)

State before:
m : ℕ
⊢ ∏ p in primes (Finset.Ioc (m + 1) (2 * m + 1)), p ≤ Nat.choose (2 * m + 1) m
Tactic:
rw [primes]
State after:
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ≤ Nat.choose (2 * m + 1) m

State before:
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ≤ Nat.choose (2 * m + 1) m
Tactic:
apply Nat.le_of_dvd
State after:
case h
m : ℕ
⊢ 0 < Nat.choose (2 * m + 1) m

case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m

State before:
case h
m : ℕ
⊢ 0 < Nat.choose (2 * m + 1) m

case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m
Tactic:
. apply Nat.choose_pos; linarith
State after:
case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m

State before:
case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m
Tactic:
apply Finset.prod_primes_dvd <;> simp [← Nat.prime_iff]
State after:
case a.div
m : ℕ
⊢ ∀ (a : ℕ), m + 1 < a → a ≤ 2 * m + 1 → Nat.Prime a → a ∣ Nat.choose (2 * m + 1) m

State before:
case a.div
m : ℕ
⊢ ∀ (a : ℕ), m + 1 < a → a ≤ 2 * m + 1 → Nat.Prime a → a ∣ Nat.choose (2 * m + 1) m
Tactic:
intro p ha hb hp
State after:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (2 * m + 1) m

State before:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (2 * m + 1) m
Tactic:
rw [two_mul, add_assoc]
State after:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (m + (m + 1)) m

State before:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (m + (m + 1)) m
Tactic:
apply Nat.Prime.dvd_choose_add hp <;> linarith
State after:
no goals

State before:
case h
m : ℕ
⊢ 0 < Nat.choose (2 * m + 1) m
Tactic:
apply Nat.choose_pos
State after:
case h.a
m : ℕ
⊢ m ≤ 2 * m + 1

State before:
case h.a
m : ℕ
⊢ m ≤ 2 * m + 1
Tactic:
linarith
State after:
no goals