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

State before:
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
by_cases h : p ≤ 2 * n
State after:
case pos
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case neg
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : ¬p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

State before:
case pos
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact ⟨p, prime_p, hn, h⟩
State after:
no goals

State before:
case neg
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : ¬p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact H (lt_of_mul_lt_mul_left' (lt_of_lt_of_le (not_le.1 h) covering))
State after:
no goals