internlm/Lean-Github huggingface dataset:
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro.inr.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases nmp : (n / m).Prime
Proof state after:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : (n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : ¬(n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : ¬(n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases ih (n / m) nmltn h1 nmp with ⟨p, pp, pdvd, p4eq⟩
Proof state after:
case neg.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : ¬(n / m).Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : ¬(n / m).Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use p
Proof state after:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : ¬(n / m).Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : ¬(n / m).Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
exact ⟨pp, pdvd.trans nmdvdn, p4eq⟩
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case pos
n : ℕ
h : n % 4 = 3
np : n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use n
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ 2 ≤ m
Tactic:
apply two_le _ mne1
Proof state after:
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ m ≠ 0
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
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, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
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_mod_4_eq_3
Proof state before:
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
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, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
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_mod_4_eq_3
Proof state before:
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
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_mod_4_eq_3
Proof state before:
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
⊢ m % 4 = 3 ∨ n / m % 4 = 3
Tactic:
apply mod_4_eq_3_or_mod_4_eq_3
Proof state after:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
⊢ m * (n / m) % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
⊢ m * (n / m) % 4 = 3
Tactic:
rw [neq, h]
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro.inl
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases mp : m.Prime
Proof state after:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases ih m mltn h1 mp with ⟨p, pp, pdvd, p4eq⟩
Proof state after:
case neg.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use p
Proof state after:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
exact ⟨pp, pdvd.trans mdvdn, p4eq⟩
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
mp : m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use m
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
nmp : (n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use n / m
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
⊢ ∀ (n : ℕ), ∃ p > n, p.Prime ∧ p % 4 = 3
Tactic:
by_contra h
Proof state after:
h : ¬∀ (n : ℕ), ∃ p > n, p.Prime ∧ p % 4 = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
h : ¬∀ (n : ℕ), ∃ p > n, p.Prime ∧ p % 4 = 3
⊢ False
Tactic:
push_neg  at h
Proof state after:
h : ∃ n, ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
h : ∃ n, ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ False
Tactic:
rcases h with ⟨n, hn⟩
Proof state after:
case intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ False
Tactic:
have : ∃ s : Finset Nat, ∀ p : ℕ, p.Prime ∧ p % 4 = 3 ↔ p ∈ s := by
  apply ex_finset_of_bounded
  use n
  contrapose! hn
  rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
  exact ⟨p, pltn, pp, p4⟩
Proof state after:
case intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
this : ∃ s, ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
this : ∃ s, ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ False
Tactic:
rcases this with ⟨s, hs⟩
Proof state after:
case intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ False
Tactic:
have h₁ : ((4 * ∏ i in erase s 3, i) + 3) % 4 = 3 := by
  rw [add_comm, Nat.add_mul_mod_self_left]
Proof state after:
case intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
⊢ False
Tactic:
rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
⊢ False
Tactic:
have ps : p ∈ s := by
  rw [← hs p]
  exact ⟨pp, p4eq⟩
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
⊢ False
Tactic:
have pne3 : p ≠ 3 := by
  intro peq
  rw [peq, ← Nat.dvd_add_iff_left (dvd_refl 3)] at pdvd
  rw [Nat.prime_three.dvd_mul] at pdvd
  norm_num at pdvd
  have : 3 ∈ s.erase 3 := by
    apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd
    intro n
    simp [← hs n]
    tauto
  simp at this
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ False
Tactic:
have : p ∣ 4 * ∏ i in erase s 3, i := by
  apply dvd_trans _ (dvd_mul_left _ _)
  apply dvd_prod_of_mem
  simp
  constructor <;> assumption
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i ∈ s.erase 3, i
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i ∈ s.erase 3, i
⊢ False
Tactic:
have : p ∣ 3 := by
  convert Nat.dvd_sub' pdvd this
  simp
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i ∈ s.erase 3, i
this : p ∣ 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i ∈ s.erase 3, i
this : p ∣ 3
⊢ False
Tactic:
have : p = 3 := by
  apply pp.eq_of_dvd_of_prime Nat.prime_three this
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝¹ : p ∣ 4 * ∏ i ∈ s.erase 3, i
this✝ : p ∣ 3
this : p = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝¹ : p ∣ 4 * ∏ i ∈ s.erase 3, i
this✝ : p ∣ 3
this : p = 3
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ ∃ s, ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
Tactic:
apply ex_finset_of_bounded
Proof state after:
case a
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ ∃ n, ∀ (k : ℕ), k.Prime ∧ k % 4 = 3 → k ≤ n
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case a
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ ∃ n, ∀ (k : ℕ), k.Prime ∧ k % 4 = 3 → k ≤ n
Tactic:
use n
Proof state after:
case h
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ ∀ (k : ℕ), k.Prime ∧ k % 4 = 3 → k ≤ n
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case h
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ ∀ (k : ℕ), k.Prime ∧ k % 4 = 3 → k ≤ n
Tactic:
contrapose! hn
Proof state after:
case h
n : ℕ
hn : ∃ k, (k.Prime ∧ k % 4 = 3) ∧ n < k
⊢ ∃ p > n, p.Prime ∧ p % 4 = 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case h
n : ℕ
hn : ∃ k, (k.Prime ∧ k % 4 = 3) ∧ n < k
⊢ ∃ p > n, p.Prime ∧ p % 4 = 3
Tactic:
rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
Proof state after:
case h.intro.intro.intro
n p : ℕ
pltn : n < p
pp : p.Prime
p4 : p % 4 = 3
⊢ ∃ p > n, p.Prime ∧ p % 4 = 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case h.intro.intro.intro
n p : ℕ
pltn : n < p
pp : p.Prime
p4 : p % 4 = 3
⊢ ∃ p > n, p.Prime ∧ p % 4 = 3
Tactic:
exact ⟨p, pltn, pp, p4⟩
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
Tactic:
rw [add_comm, Nat.add_mul_mod_self_left]
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
⊢ p ∈ s
Tactic:
rw [← hs p]
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
⊢ p.Prime ∧ p % 4 = 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
⊢ p.Prime ∧ p % 4 = 3
Tactic:
exact ⟨pp, p4eq⟩
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
⊢ p ≠ 3
Tactic:
intro peq
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Tactic:
rw [peq, ← Nat.dvd_add_iff_left (dvd_refl 3)] at pdvd
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : 3 ∣ 4 * ∏ i ∈ s.erase 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : 3 ∣ 4 * ∏ i ∈ s.erase 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Tactic:
rw [Nat.prime_three.dvd_mul] at pdvd
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : 3 ∣ 4 ∨ 3 ∣ ∏ i ∈ s.erase 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : 3 ∣ 4 ∨ 3 ∣ ∏ i ∈ s.erase 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Tactic:
norm_num at pdvd
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
⊢ False
Tactic:
have : 3 ∈ s.erase 3 := by
  apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd
  intro n
  simp [← hs n]
  tauto
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
this : 3 ∈ s.erase 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
this : 3 ∈ s.erase 3
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
⊢ 3 ∈ s.erase 3
Tactic:
apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
⊢ ∀ n ∈ s.erase 3, n.Prime
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
⊢ ∀ n ∈ s.erase 3, n.Prime
Tactic:
intro n
Proof state after:
n✝ : ℕ
hn : ∀ p > n✝, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
n : ℕ
⊢ n ∈ s.erase 3 → n.Prime