Theorem: C05S03.mem_of_dvd_prod_primes (MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
s : Finset ℕ
p : ℕ
prime_p : p.Prime
⊢ (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
Tactic:
intro h₀ h₁
State after:
s : Finset ℕ
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ s, n.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s

State before:
s : Finset ℕ
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ s, n.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s
Tactic:
induction' s using Finset.induction_on with a s ans ih
State after:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p ∣ ∏ n ∈ ∅, n
⊢ p ∈ ∅

case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : ∀ n ∈ insert a s, n.Prime
h₁ : p ∣ ∏ n ∈ insert a s, n
⊢ p ∈ insert a s

State before:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : ∀ n ∈ insert a s, n.Prime
h₁ : p ∣ ∏ n ∈ insert a s, n
⊢ p ∈ insert a s
Tactic:
simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
State after:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p ∈ insert a s

State before:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p ∈ insert a s
Tactic:
rw [mem_insert]
State after:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s

State before:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s
Tactic:
rcases h₁ with h₁ | h₁
State after:
case insert.inl
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a
⊢ p = a ∨ p ∈ s

case insert.inr
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s

State before:
case insert.inr
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s
Tactic:
right
State after:
case insert.inr.h
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s

State before:
case insert.inr.h
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s
Tactic:
exact ih h₀.2 h₁
State after:
no goals

State before:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p ∣ ∏ n ∈ ∅, n
⊢ p ∈ ∅
Tactic:
simp at h₁
State after:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p = 1
⊢ p ∈ ∅

State before:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p = 1
⊢ p ∈ ∅
Tactic:
linarith [prime_p.two_le]
State after:
no goals

State before:
case insert.inl
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a
⊢ p = a ∨ p ∈ s
Tactic:
left
State after:
case insert.inl.h
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a
⊢ p = a

State before:
case insert.inl.h
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a
⊢ p = a
Tactic:
exact prime_p.eq_of_dvd_of_prime h₀.1 h₁
State after:
no goals