internlm/Lean-Github huggingface dataset:
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:
rcases h₁ with h₁ | h₁
Proof state after:
case insert.inl
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 = a ∨ p ∈ s

case insert.inr
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 ∣ ∏ n in s, n
⊢ p = a ∨ p ∈ s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert.inr
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 ∣ ∏ n in s, n
⊢ p = a ∨ p ∈ s
Tactic:
right
Proof state after:
case insert.inr.h
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 ∣ ∏ n in s, n
⊢ p ∈ s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert.inr.h
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 ∣ ∏ n in s, n
⊢ p ∈ s
Tactic:
exact ih h₀.2 h₁
Proof state after:
no goals
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert.inl
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 = a ∨ p ∈ s
Tactic:
left
Proof state after:
case insert.inl.h
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 = a
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert.inl.h
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 = a
Tactic:
exact prime_p.eq_of_dvd_of_prime h₀.1 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
⊢ 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
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:
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
  apply dvd_prod_of_mem
  rw [mem_s']
  apply pp
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
this : p ∣ 1
⊢ False
Tactic:
have := Nat.le_of_dvd zero_lt_one this
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
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
this : p ≤ 1
⊢ False
Tactic:
linarith [pp.two_le]
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:
apply Nat.succ_le_succ
Proof state after:
case a
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
⊢ 1 ≤ ∏ i in s', i
Theorem: C05S03.primes_infinite'
Proof state before:
case a
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
⊢ 1 ≤ ∏ i in s', i
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case a.h
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
⊢ 0 < ∏ i in s', i
Theorem: C05S03.primes_infinite'
Proof state before:
case a.h
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
⊢ 0 < ∏ i in s', i
Tactic:
apply Finset.prod_pos
Proof state after:
case a.h.h0
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
⊢ ∀ i ∈ s', 0 < i
Theorem: C05S03.primes_infinite'
Proof state before:
case a.h.h0
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
⊢ ∀ i ∈ s', 0 < i
Tactic:
intro n ns'
Proof state after:
case a.h.h0
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
n : ℕ
ns' : n ∈ s'
⊢ 0 < n
Theorem: C05S03.primes_infinite'
Proof state before:
case a.h.h0
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
n : ℕ
ns' : n ∈ s'
⊢ 0 < n
Tactic:
apply (mem_s'.mp ns').pos
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:
apply dvd_prod_of_mem
Proof state after:
case ha
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 ∈ s'
Theorem: C05S03.primes_infinite'
Proof state before:
case ha
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 ∈ s'
Tactic:
rw [mem_s']
Proof state after:
case ha
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
⊢ Nat.Prime p
Theorem: C05S03.primes_infinite'
Proof state before:
case ha
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
⊢ Nat.Prime p
Tactic:
apply pp
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro.inr
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn
Proof state after:
case neg.h.intro.intro.intro.inr.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases nmp : (n / m).Prime
Proof state after:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : Nat.Prime (n / m)
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime (n / m)
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime (n / m)
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime (n / m)
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime (n / m)
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use p
Proof state after:
case 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 : 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 : ¬Nat.Prime (n / m)
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime (n / m)
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ Nat.Prime p ∧ 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 neg.h.intro.intro.intro.inl
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases mp : m.Prime
Proof state after:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use p
Proof state after:
case 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 : 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 : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ 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 : Nat.Prime (n / m)
⊢ ∃ p, Nat.Prime p ∧ 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:
case intro.intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ 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]
  norm_num
Proof state after:
case intro.intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i in erase s 3, i
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝¹ : p ∣ 4 * ∏ i in erase s 3, i
this✝ : p ∣ 3
this : p = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
⊢ (4 * ∏ i in erase s 3, i + 3) % 4 = 3
Tactic:
rw [add_comm, Nat.add_mul_mod_self_left]
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
⊢ 3 % 4 = 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
⊢ 3 % 4 = 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
⊢ p ∈ s
Tactic:
rw [← hs p]
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
⊢ Nat.Prime p ∧ p % 4 = 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
⊢ Nat.Prime p ∧ 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
⊢ p ≠ 3
Tactic:
intro peq
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 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, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : 3 ∣ 4 * ∏ i in erase s 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False