cases lt_or_le n 4000 with
| inl hn' => exact landauTrick (by linarith) (by linarith)
| inr hn' =>
  by_contra h
  simp at h
  replace h : ∏ p in primes (Finset.Ioc n (2*n)), p = 1
  . apply Finset.prod_eq_one
    intro i hi
    specialize h i
    simp [primes] at *
    specialize h hi.left.left hi.left.right hi.right
    contradiction
  have h' := fourPowLeMulProdPrimes (by linarith : 2 < n)
  simp [h] at h'; clear h
  replace h' := rpowDivThreeLe (by linarith : 0 < n) h'
  have : (81 / 2 : ℝ) < ↑n
  . rw [div_lt_iff (by norm_num)]; norm_cast; linarith
  replace h' := fourPowLtOf this h'; clear this
  rw [lt4kIff (by norm_cast)] at h'
  norm_cast at h'
  linarith
n : ℕ
hn : 0 < n
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
no goals