Theorem: HTPI.all_prime_nil (HTPILib/Chap7.lean)

State before:
⊢ all_prime []
Tactic:
define
State after:
⊢ ∀ p ∈ [], prime p

State before:
⊢ ∀ p ∈ [], prime p
Tactic:
fix p : Nat
State after:
p : ℕ
⊢ p ∈ [] → prime p

State before:
p : ℕ
⊢ p ∈ [] → prime p
Tactic:
contrapos
State after:
p : ℕ
⊢ ¬prime p → p ∉ []

State before:
p : ℕ
⊢ ¬prime p → p ∉ []
Tactic:
assume h1 : ¬prime p
State after:
p : ℕ
h1 : ¬prime p
⊢ p ∉ []

State before:
p : ℕ
h1 : ¬prime p
⊢ p ∉ []
Tactic:
show p ∉ [] from List.not_mem_nil p
State after:
no goals