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

State before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : all_prime l
h3 : p ∣ prod l
⊢ p ∈ l
Tactic:
obtain (a : Nat) (h4 : a ∈ l ∧ p ∣ a) from Theorem_7_2_4 h1 l h3
State after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : all_prime l
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l

State before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : all_prime l
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l
Tactic:
define at h2
State after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l

State before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l
Tactic:
have h5 : prime a := h2 a h4.left
State after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
⊢ p ∈ l

State before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
⊢ p ∈ l
Tactic:
have h6 : p = 1 ∨ p = a := dvd_prime h5 h4.right
State after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = 1 ∨ p = a
⊢ p ∈ l

State before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = 1 ∨ p = a
⊢ p ∈ l
Tactic:
disj_syll h6 (prime_not_one h1)
State after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ p ∈ l

State before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ p ∈ l
Tactic:
rewrite [h6]
State after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ a ∈ l

State before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ a ∈ l
Tactic:
show a ∈ l from h4.left
State after:
no goals