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

State before:
l : List ℕ
h : nondec_prime_list l
⊢ l = [] ↔ prod l = 1
Tactic:
apply Iff.intro
State after:
case mp
l : List ℕ
h : nondec_prime_list l
⊢ l = [] → prod l = 1

case mpr
l : List ℕ
h : nondec_prime_list l
⊢ prod l = 1 → l = []

State before:
case mp
l : List ℕ
h : nondec_prime_list l
⊢ l = [] → prod l = 1
Tactic:
assume h1 : l = []
State after:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod l = 1

State before:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod l = 1
Tactic:
rewrite [h1]
State after:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod [] = 1

State before:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod [] = 1
Tactic:
show prod [] = 1 from prod_nil
State after:
no goals

State before:
case mpr
l : List ℕ
h : nondec_prime_list l
⊢ prod l = 1 → l = []
Tactic:
contrapos
State after:
case mpr
l : List ℕ
h : nondec_prime_list l
⊢ ¬l = [] → ¬prod l = 1

State before:
case mpr
l : List ℕ
h : nondec_prime_list l
⊢ ¬l = [] → ¬prod l = 1
Tactic:
assume h1 : ¬l = []
State after:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
⊢ ¬prod l = 1

State before:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
⊢ ¬prod l = 1
Tactic:
obtain (p : Nat) (h2 : ∃ (L : List Nat), l = p :: L) from
  List.exists_cons_of_ne_nil h1
State after:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
⊢ ¬prod l = 1

State before:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
⊢ ¬prod l = 1
Tactic:
obtain (L : List Nat) (h3 : l = p :: L) from h2
State after:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h3 : l = p :: L
⊢ ¬prod l = 1

State before:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h3 : l = p :: L
⊢ ¬prod l = 1
Tactic:
rewrite [h3] at h
State after:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod l = 1

State before:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod l = 1
Tactic:
rewrite [h3]
State after:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod (p :: L) = 1

State before:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod (p :: L) = 1
Tactic:
show ¬prod (p :: L) = 1 from cons_prod_not_one h
State after:
no goals