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

State before:
p : ℕ
l : List ℕ
h : nondec_prime_list (p :: l)
⊢ nondec_prime_list l
Tactic:
define at h
State after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ nondec_prime_list l

State before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ nondec_prime_list l
Tactic:
define
State after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ all_prime l ∧ nondec l

State before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ all_prime l ∧ nondec l
Tactic:
rewrite [all_prime_cons, nondec_cons] at h
State after:
p : ℕ
l : List ℕ
h : (prime p ∧ all_prime l) ∧ (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ all_prime l ∧ nondec l

State before:
p : ℕ
l : List ℕ
h : (prime p ∧ all_prime l) ∧ (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ all_prime l ∧ nondec l
Tactic:
show all_prime l ∧ nondec l from And.intro h.left.right h.right.right
State after:
no goals