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

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

State before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ prod (p :: l) ≠ 1
Tactic:
have h1 : all_prime (p :: l) := h.left
State after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : all_prime (p :: l)
⊢ prod (p :: l) ≠ 1

State before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : all_prime (p :: l)
⊢ prod (p :: l) ≠ 1
Tactic:
rewrite [all_prime_cons] at h1
State after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ prod (p :: l) ≠ 1

State before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ prod (p :: l) ≠ 1
Tactic:
rewrite [prod_cons]
State after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ p * prod l ≠ 1

State before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ p * prod l ≠ 1
Tactic:
by_contra h2
State after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
h2 : p * prod l = 1
⊢ False

State before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
h2 : p * prod l = 1
⊢ False
Tactic:
show False from (prime_not_one h1.left) (eq_one_of_prod_one h2)
State after:
no goals