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

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

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

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

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

State before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → 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 : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ False

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

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

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

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

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

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

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

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

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

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

State before:
case a
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 1 ≤ ∏ i ∈ s', i
Tactic:
apply Nat.succ_le_of_lt
State after:
case a.h
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 0 < ∏ i ∈ s', i

State before:
case a.h
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 0 < ∏ i ∈ s', i
Tactic:
apply Finset.prod_pos
State after:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ ∀ i ∈ s', 0 < i

State before:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ ∀ i ∈ s', 0 < i
Tactic:
intro n ns'
State after:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
n : ℕ
ns' : n ∈ s'
⊢ 0 < n

State before:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
n : ℕ
ns' : n ∈ s'
⊢ 0 < n
Tactic:
apply (mem_s'.mp ns').pos
State after:
no goals

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

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

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

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

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