p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p
by_contra' h
p : ℕ
h : p < 5
⊢ Prime p → p ≠ 2 → p ≠ 3 → False
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False
revert h_two h_three hp
no goals
p : ℕ
h : p < 5
⊢ Prime p → p ≠ 2 → p ≠ 3 → False
match p with
| 0 => decide
| 1 => decide
| 2 => decide
| 3 => decide
| 4 => decide
| n + 5 => exact (h.not_le le_add_self).elim
no goals
p : ℕ
h : 0 < 5
⊢ Prime 0 → 0 ≠ 2 → 0 ≠ 3 → False
decide
no goals
p : ℕ
h : 1 < 5
⊢ Prime 1 → 1 ≠ 2 → 1 ≠ 3 → False
decide
no goals
p : ℕ
h : 2 < 5
⊢ Prime 2 → 2 ≠ 2 → 2 ≠ 3 → False
decide
no goals
p : ℕ
h : 3 < 5
⊢ Prime 3 → 3 ≠ 2 → 3 ≠ 3 → False
decide
no goals
p : ℕ
h : 4 < 5
⊢ Prime 4 → 4 ≠ 2 → 4 ≠ 3 → False
decide
no goals
p n : ℕ
h : n + 5 < 5
⊢ Prime (n + 5) → n + 5 ≠ 2 → n + 5 ≠ 3 → False
exact (h.not_le le_add_self).elim