internlm/Lean-Github huggingface dataset:
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg
n : ℕ
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
induction' n using Nat.strong_induction_on with n ih
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
rw [Nat.prime_def_lt] at np
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
push_neg at np
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
rcases np h with ⟨m, mltn, mdvdn, mne1⟩
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
have : m ≠ 0 := by
  intro mz
  rw [mz, zero_dvd_iff] at mdvdn
  linarith
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
have mgt2 : 2 ≤ m := two_le this mne1
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
by_cases mp : m.Prime
Proof state after:
case pos
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
. rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
  use p, pp
  apply pdvd.trans mdvdn
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
case pos
n : ℕ
h : 2 ≤ n
np : Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
use n, np
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ m ≠ 0
Tactic:
intro mz
Proof state after:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mz : m = 0
⊢ False
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mz : m = 0
⊢ False
Tactic:
rw [mz, zero_dvd_iff] at mdvdn
Proof state after:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : n = 0
mne1 : m ≠ 1
mz : m = 0
⊢ False
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : n = 0
mne1 : m ≠ 1
mz : m = 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
case pos
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
use m, mp
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
Proof state after:
case neg.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
use p, pp
Proof state after:
case right
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case right
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ p ∣ n
Tactic:
apply pdvd.trans mdvdn
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
⊢ ∀ (n : ℕ), ∃ p > n, Nat.Prime p
Tactic:
intro n
Proof state after:
n : ℕ
⊢ ∃ p > n, Nat.Prime p
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
⊢ ∃ p > n, Nat.Prime p
Tactic:
have : 2 ≤ Nat.factorial (n + 1) + 1 := by
  sorry
Proof state after:
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
⊢ ∃ p > n, Nat.Prime p
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
⊢ ∃ p > n, Nat.Prime p
Tactic:
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
⊢ ∃ p > n, Nat.Prime p
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
⊢ ∃ p > n, Nat.Prime p
Tactic:
refine' ⟨p, _, pp⟩
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
⊢ p > n
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
⊢ p > n
Tactic:
by_contra ple
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : ¬p > n
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : ¬p > n
⊢ False
Tactic:
push_neg  at ple
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
⊢ False
Tactic:
have : p ∣ Nat.factorial (n + 1) := by
  sorry
Proof state after:
case intro.intro
n : ℕ
this✝ : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
this : p ∣ Nat.factorial (n + 1)
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this✝ : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
this : p ∣ Nat.factorial (n + 1)
⊢ False
Tactic:
have : p ∣ 1 := by
  sorry
Proof state after:
case intro.intro
n : ℕ
this✝¹ : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
this✝ : p ∣ Nat.factorial (n + 1)
this : p ∣ 1
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this✝¹ : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
this✝ : p ∣ Nat.factorial (n + 1)
this : p ∣ 1
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
⊢ 2 ≤ Nat.factorial (n + 1) + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
⊢ p ∣ Nat.factorial (n + 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
this✝ : 2 ≤ Nat.factorial (n + 1) + 1
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ Nat.factorial (n + 1) + 1
ple : p ≤ n
this : p ∣ Nat.factorial (n + 1)
⊢ p ∣ 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Nat.Prime.eq_of_dvd_of_prime
Proof state before:
p q : ℕ
prime_p : Nat.Prime p
prime_q : Nat.Prime q
h : p ∣ q
⊢ p = q
Tactic:
sorry
Proof state after:
no goals
Theorem: C05S03.mem_of_dvd_prod_primes
Proof 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₁
Proof state after:
s : Finset ℕ
p : ℕ
prime_p : Nat.Prime p
h₀ : ∀ n ∈ s, Nat.Prime n
h₁ : p ∣ ∏ n in s, n
⊢ p ∈ s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof 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
Proof 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
Theorem: C05S03.mem_of_dvd_prod_primes
Proof 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₁
Proof 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
Theorem: C05S03.mem_of_dvd_prod_primes
Proof 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]
Proof 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
Theorem: C05S03.mem_of_dvd_prod_primes
Proof 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
Proof state after:
no goals
Theorem: C05S03.mem_of_dvd_prod_primes
Proof 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₁
Proof state after:
case empty
p : ℕ
prime_p : Nat.Prime p
h₀ : ∀ n ∈ ∅, Nat.Prime n
h₁ : p = 1
⊢ p ∈ ∅
Theorem: C05S03.mem_of_dvd_prod_primes
Proof 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]
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof state before:
⊢ ∀ (s : Finset ℕ), ∃ p, Nat.Prime p ∧ p ∉ s
Tactic:
intro s
Proof state after:
s : Finset ℕ
⊢ ∃ p, Nat.Prime p ∧ p ∉ s
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
⊢ ∃ p, Nat.Prime p ∧ p ∉ s
Tactic:
by_contra h
Proof state after:
s : Finset ℕ
h : ¬∃ p, Nat.Prime p ∧ p ∉ s
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ¬∃ p, Nat.Prime p ∧ p ∉ s
⊢ False
Tactic:
push_neg  at h
Proof state after:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), Nat.Prime p → p ∈ s
⊢ False
Tactic:
set s' := s.filter Nat.Prime with s'_def
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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⟩
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof 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
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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]
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof 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
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof 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
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof 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
Proof 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
Theorem: C05S03.primes_infinite'
Proof 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
Proof state after:
no goals
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case intro
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∃ n, ∀ (k : ℕ), Q k → k < n
Tactic:
use s.sup id + 1
Proof state after:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∀ (k : ℕ), Q k → k < sup s id + 1
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∀ (k : ℕ), Q k → k < sup s id + 1
Tactic:
intro k Qk
Proof state after:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k < sup s id + 1
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k < sup s id + 1
Tactic:
apply Nat.lt_succ_of_le
Proof state after:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k ≤ sup s id
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k ≤ sup s id
Tactic:
show id k ≤ s.sup id
Proof state after:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ id k ≤ sup s id
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ id k ≤ sup s id
Tactic:
apply le_sup (hs k Qk)
Proof state after:
no goals
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
this : m % 4 < 4
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Tactic:
interval_cases hm : m % 4 <;> simp [hm]
Proof state after:
case «2»
m n : ℕ
hm : m % 4 = 2
this : 2 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
case «2»
m n : ℕ
hm : m % 4 = 2
this : 2 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Tactic:
have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
Proof state after:
case «2»
m n : ℕ
hm : m % 4 = 2
this✝ : 2 < 4
this : n % 4 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
case «2»
m n : ℕ
hm : m % 4 = 2
this✝ : 2 < 4
this : n % 4 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Tactic:
interval_cases hn : n % 4 <;> simp [hn]
Proof state after:
no goals
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
hm : m % 4 = 2
this : 2 < 4
⊢ 4 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: C05S03.aux
Proof state before:
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n ∧ n / m < n
Tactic:
sorry
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
n : ℕ
h : n % 4 = 3
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases np : n.Prime
Proof state after:
case pos
n : ℕ
h : n % 4 = 3
np : Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
h : n % 4 = 3
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg
n : ℕ
h : n % 4 = 3
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
induction' n using Nat.strong_induction_on with n ih
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3