Theorem: chapter02.exists_prime_lt_and_le_two_mul (FormalBook/Chapter_02.lean)

State before:
n : ℕ
hn0 : n ≠ 0
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
cases' lt_or_le 511 n with h h
State after:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

State before:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
swap
State after:
case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

State before:
case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
replace h : n < 521 := h.trans_lt (by norm_num1)
State after:
case inr
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

State before:
case inr
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
revert h
State after:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

State before:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
open Lean Elab Tactic in
run_tac do
  for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
    let i : Term := quote i
    evalTactic <| ←
      `(tactic| refine' exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) _)
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩
State after:
no goals

State before:
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ 511 < 521
Tactic:
norm_num1
State after:
no goals

State before:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
run_tac do
  for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
    let i : Term := quote i
    evalTactic <| ←
      `(tactic| refine' exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) _)
State after:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 2 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

State before:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 2 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩
State after:
no goals

State before:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact exists_prime_lt_and_le_two_mul_eventually n h
State after:
no goals