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

State before:
p : ℕ
h1 : prime p
⊢ ∀ (l : List ℕ), p ∣ prod l → ∃ a ∈ l, p ∣ a
Tactic:
apply List.rec
State after:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ prod [] → ∃ a ∈ [], p ∣ a

case cons
p : ℕ
h1 : prime p
⊢ ∀ (head : ℕ) (tail : List ℕ),
    (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (head :: tail) → ∃ a ∈ head :: tail, p ∣ a

State before:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ prod [] → ∃ a ∈ [], p ∣ a
Tactic:
rewrite [prod_nil]
State after:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ 1 → ∃ a ∈ [], p ∣ a

State before:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ 1 → ∃ a ∈ [], p ∣ a
Tactic:
assume h2 : p ∣ 1
State after:
case nil
p : ℕ
h1 : prime p
h2 : p ∣ 1
⊢ ∃ a ∈ [], p ∣ a

State before:
case nil
p : ℕ
h1 : prime p
h2 : p ∣ 1
⊢ ∃ a ∈ [], p ∣ a
Tactic:
show ∃ a ∈ [], p ∣ a from
  absurd (eq_one_of_dvd_one h2) (prime_not_one h1)
State after:
no goals

State before:
case cons
p : ℕ
h1 : prime p
⊢ ∀ (head : ℕ) (tail : List ℕ),
    (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (head :: tail) → ∃ a ∈ head :: tail, p ∣ a
Tactic:
fix b : Nat
State after:
case cons
p : ℕ
h1 : prime p
b : ℕ
⊢ ∀ (tail : List ℕ), (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (b :: tail) → ∃ a ∈ b :: tail, p ∣ a

State before:
case cons
p : ℕ
h1 : prime p
b : ℕ
⊢ ∀ (tail : List ℕ), (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (b :: tail) → ∃ a ∈ b :: tail, p ∣ a
Tactic:
fix L : List Nat
State after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
⊢ (p ∣ prod L → ∃ a ∈ L, p ∣ a) → p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a

State before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
⊢ (p ∣ prod L → ∃ a ∈ L, p ∣ a) → p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
Tactic:
assume ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
State after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
⊢ p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a

State before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
⊢ p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
Tactic:
assume h2 : p ∣ prod (b :: L)
State after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ prod (b :: L)
⊢ ∃ a ∈ b :: L, p ∣ a

State before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ prod (b :: L)
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
rewrite [prod_cons] at h2
State after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
⊢ ∃ a ∈ b :: L, p ∣ a

State before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
have h3 : p ∣ b ∨ p ∣ prod L := Theorem_7_2_3 h1 h2
State after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b ∨ p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a

State before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b ∨ p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
by_cases on h3
State after:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ ∃ a ∈ b :: L, p ∣ a

case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a

State before:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
apply Exists.intro b
State after:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ b ∈ b :: L ∧ p ∣ b

State before:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ b ∈ b :: L ∧ p ∣ b
Tactic:
show b ∈ b :: L ∧ p ∣ b from
  And.intro (List.mem_cons_self b L) h3
State after:
no goals

State before:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
obtain (a : Nat) (h4 : a ∈ L ∧ p ∣ a) from ih h3
State after:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ ∃ a ∈ b :: L, p ∣ a

State before:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
apply Exists.intro a
State after:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ a ∈ b :: L ∧ p ∣ a

State before:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ a ∈ b :: L ∧ p ∣ a
Tactic:
show a ∈ b :: L ∧ p ∣ a from
  And.intro (List.mem_cons_of_mem b h4.left) h4.right
State after:
no goals