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

State before:
⊢ ∀ (s : Finset ℕ), ∃ p, Nat.Prime p ∧ p ∉ s
Tactic:
intro s
State after:
s : Finset ℕ
⊢ ∃ p, Nat.Prime p ∧ p ∉ s

State before:
s : Finset ℕ
⊢ ∃ p, Nat.Prime p ∧ p ∉ s
Tactic:
by_contra h
State after:
s : Finset ℕ
h : ¬∃ p, Nat.Prime p ∧ p ∉ s
⊢ False

State before:
s : Finset ℕ
h : ¬∃ p, Nat.Prime p ∧ p ∉ s
⊢ False
Tactic:
push_neg  at h
State after:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
⊢ False

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
⊢ False
Tactic:
set s' := s.filter Nat.Prime with s'_def
State after:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ False

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ False
Tactic:
have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime := by
  intro n
  simp [s'_def]
  apply h
State after:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
⊢ False

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
⊢ False
Tactic:
have : 2 ≤ (∏ i in s', i) + 1 := by
  sorry
State after:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this : 2 ≤ ∏ i in s', i + 1
⊢ False

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this : 2 ≤ ∏ i in s', i + 1
⊢ False
Tactic:
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
State after:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
⊢ False

State before:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
⊢ False
Tactic:
have : p ∣ ∏ i in s', i := by
  sorry
State after:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this✝ : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
this : p ∣ ∏ i in s', i
⊢ False

State before:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this✝ : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
this : p ∣ ∏ i in s', i
⊢ False
Tactic:
have : p ∣ 1 := by
  convert Nat.dvd_sub' pdvd this
  simp
State after:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this✝¹ : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
this✝ : p ∣ ∏ i in s', i
this : p ∣ 1
⊢ False

State before:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this✝¹ : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
this✝ : p ∣ ∏ i in s', i
this : p ∣ 1
⊢ False
Tactic:
sorry
State after:
no goals

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
Tactic:
intro n
State after:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ n ∈ s' ↔ Nat.Prime n

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ n ∈ s' ↔ Nat.Prime n
Tactic:
simp [s'_def]
State after:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ Nat.Prime n → n ∈ s

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ Nat.Prime n → n ∈ s
Tactic:
apply h
State after:
no goals

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
⊢ 2 ≤ ∏ i in s', i + 1
Tactic:
sorry
State after:
no goals

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
⊢ p ∣ ∏ i in s', i
Tactic:
sorry
State after:
no goals

State before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this✝ : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
this : p ∣ ∏ i in s', i
⊢ p ∣ 1
Tactic:
convert Nat.dvd_sub' pdvd this
State after:
case h.e'_4
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this✝ : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
this : p ∣ ∏ i in s', i
⊢ 1 = ∏ i in s', i + 1 - ∏ i in s', i

State before:
case h.e'_4
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ Nat.Prime n
this✝ : 2 ≤ ∏ i in s', i + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ ∏ i in s', i + 1
this : p ∣ ∏ i in s', i
⊢ 1 = ∏ i in s', i + 1 - ∏ i in s', i
Tactic:
simp
State after:
no goals