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

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

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

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

State before:
case insert
p : ℕ
prime_p : Nat.Prime p
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, Nat.Prime n) → p ∣ ∏ n in s, n → p ∈ s
h₀ : ∀ n ∈ insert a s, Nat.Prime n
h₁ : p ∣ ∏ n in 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 : Nat.Prime p
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, Nat.Prime n) → p ∣ ∏ n in s, n → p ∈ s
h₀ : Nat.Prime a ∧ ∀ a ∈ s, Nat.Prime a
h₁ : p ∣ a ∨ p ∣ ∏ n in s, n
⊢ p ∈ insert a s

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

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

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

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