internlm/Lean-Github huggingface dataset:
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
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
Tactic:
rw [Nat.prime_def_lt] at np
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 : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
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 : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
push_neg  at np
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 : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
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 : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩
Proof state after:
case neg.h.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
⊢ ∃ 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
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
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
have mge2 : 2 ≤ m := by
  apply two_le _ mne1
  intro mz
  rw [mz, zero_dvd_iff] at mdvdn
  linarith
Proof state after:
case neg.h.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
⊢ ∃ 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
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
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn
Proof state after:
case neg.h.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
⊢ ∃ 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
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
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
have : m % 4 = 3 ∨ n / m % 4 = 3 := by
  apply mod_4_eq_3_or_mod_4_eq_3
  rw [neq, h]
Proof state after:
case neg.h.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
this : m % 4 = 3 ∨ n / m % 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.h.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
this : m % 4 = 3 ∨ n / m % 4 = 3
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases this with h1 | h1
Proof state after:
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

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
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

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:
. sorry
Proof state after:
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
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:
. sorry
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 : Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ 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 → ¬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
⊢ 2 ≤ m
Tactic:
apply two_le _ mne1
Proof state after:
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
⊢ m ≠ 0
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
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
⊢ m ≠ 0
Tactic:
intro mz
Proof state after:
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
mz : m = 0
⊢ False
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
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
mz : m = 0
⊢ False
Tactic:
rw [mz, zero_dvd_iff] at mdvdn
Proof state after:
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 : 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 → ¬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 : 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 → ¬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
⊢ 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 → ¬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
⊢ 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 → ¬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
⊢ 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 → ¬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:
sorry
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:
sorry
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
⊢ ∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ p % 4 = 3
Tactic:
by_contra h
Proof state after:
h : ¬∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ p % 4 = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
h : ¬∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ p % 4 = 3
⊢ False
Tactic:
push_neg  at h
Proof state after:
h : ∃ n, ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
h : ∃ n, ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ False
Tactic:
rcases h with ⟨n, hn⟩
Proof state after:
case intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → 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, Nat.Prime p → p % 4 ≠ 3
this : ∃ s, ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
this : ∃ s, ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
⊢ False
Tactic:
rcases this with ⟨s, hs⟩
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
⊢ False
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
  sorry
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
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
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, 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
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
  sorry
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
  sorry
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
  sorry
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
  sorry
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
  sorry
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:
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
Tactic:
contradiction
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, ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
Tactic:
apply ex_finset_of_bounded
Proof state after:
case a
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ ∃ n, ∀ (k : ℕ), Nat.Prime k ∧ k % 4 = 3 → k ≤ n
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case a
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ ∃ n, ∀ (k : ℕ), Nat.Prime k ∧ k % 4 = 3 → k ≤ n
Tactic:
use n
Proof state after:
case h
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ ∀ (k : ℕ), Nat.Prime k ∧ k % 4 = 3 → k ≤ n
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case h
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ ∀ (k : ℕ), Nat.Prime k ∧ k % 4 = 3 → k ≤ n
Tactic:
contrapose! hn
Proof state after:
case h
n : ℕ
hn : ∃ k, (Nat.Prime k ∧ k % 4 = 3) ∧ n < k
⊢ ∃ p > n, Nat.Prime p ∧ p % 4 = 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case h
n : ℕ
hn : ∃ k, (Nat.Prime k ∧ k % 4 = 3) ∧ n < k
⊢ ∃ p > n, Nat.Prime p ∧ 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 : Nat.Prime p
p4 : p % 4 = 3
⊢ ∃ p > n, Nat.Prime p ∧ 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 : Nat.Prime p
p4 : p % 4 = 3
⊢ ∃ p > n, Nat.Prime p ∧ 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, 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:
sorry
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:
sorry
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:
sorry
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
pne3 : p ≠ 3
⊢ p ∣ 4 * ∏ i in erase s 3, i
Tactic:
sorry
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
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i in erase s 3, i
⊢ p ∣ 3
Tactic:
sorry
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
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i in erase s 3, i
this : p ∣ 3
⊢ p = 3
Tactic:
sorry
Proof state after:
no goals
Theorem: Point.add_comm
Proof state before:
n : ℕ
a b : Point
⊢ add a b = add b a
Tactic:
simp [add, add_comm]
Proof state after:
no goals
Theorem: Point.add_x
Proof state before:
n : ℕ
a b : Point
⊢ (a + b).x = a.x + b.x
Tactic:
rfl
Proof state after:
no goals
Theorem: Point.add_y
Proof state before:
n : ℕ
a b : Point
⊢ (a + b).y = a.y + b.y
Tactic:
rfl
Proof state after:
no goals
Theorem: Point.add_z
Proof state before:
n : ℕ
a b : Point
⊢ (a + b).z = a.z + b.z
Tactic:
rfl
Proof state after:
no goals
Theorem: AbelianGroup.zero_add
Proof state before:
n : ℕ
g : AbelianGroup
x : g.G
⊢ add g g.zero x = x
Tactic:
rw [g.comm, g.add_zero]
Proof state after:
no goals
Theorem: PointedFunction.comp
Proof state before:
n : ℕ
X : PointedType
Y : PointedType
Z : PointedType
g : Y →. Z
f : X →. Y
⊢ (↑g ∘ ↑f) X.pt = Z.pt
Tactic:
sorry
Proof state after:
no goals
Theorem: fac_zero
Proof state before:
n : ℕ
⊢ fac 0 = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: fac_succ
Proof state before:
n✝ n : ℕ
⊢ fac (n + 1) = (n + 1) * fac n
Tactic:
sorry
Proof state after:
no goals
Theorem: fac_pos
Proof state before:
n✝ n : ℕ
⊢ 0 < fac n
Tactic:
sorry
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
n✝ n : ℕ
⊢ 2 ^ n ≤ fac (n + 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: sum_id
Proof state before:
n✝ n : ℕ
⊢ ∑ i in Finset.range (n + 1), i = n * (n + 1) / 2
Tactic:
sorry
Proof state after:
no goals
Theorem: coe_fib_eq
Proof state before:
n✝ n : ℕ
⊢ ↑(fib n) = (ϕ ^ n - ψ ^ n) / (ϕ - ψ)
Tactic:
sorry
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
⊢ {s | IsOpen s} ⊆ {s | IsOpen s}
Tactic:
sorry
Proof state after:
no goals
Theorem: RegularOpens.le_def
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
⊢ U ≤ V ↔ ↑U ⊆ ↑V
Tactic:
simp
Proof state after:
no goals
Theorem: RegularOpens.cl_le_iff
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V U : RegularOpens X
C : Closeds X
⊢ cl U ≤ C ↔ U ≤ Closeds.int C
Tactic:
sorry
Proof state after:
no goals
Theorem: RegularOpens.cl_int
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
⊢ Closeds.int (cl U) = U
Tactic:
sorry
Proof state after:
no goals
Theorem: RegularOpens.coe_inf
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
⊢ ↑(U ⊓ V) = ↑U ∩ ↑V
Tactic:
have : U ⊓ V = (U.cl ⊓ V.cl).int := rfl
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
this : U ⊓ V = Closeds.int (cl U ⊓ cl V)
⊢ ↑(U ⊓ V) = ↑U ∩ ↑V
Theorem: RegularOpens.coe_inf
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
this : U ⊓ V = Closeds.int (cl U ⊓ cl V)
⊢ ↑(U ⊓ V) = ↑U ∩ ↑V
Tactic:
simp [this]
Proof state after:
no goals
Theorem: RegularOpens.coe_sup
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
⊢ ↑(U ⊔ V) = interior (closure (↑U ∪ ↑V))
Tactic:
have : U ⊔ V = (U.cl ⊔ V.cl).int := rfl
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
this : U ⊔ V = Closeds.int (cl U ⊔ cl V)
⊢ ↑(U ⊔ V) = interior (closure (↑U ∪ ↑V))
Theorem: RegularOpens.coe_sup
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
this : U ⊔ V = Closeds.int (cl U ⊔ cl V)
⊢ ↑(U ⊔ V) = interior (closure (↑U ∪ ↑V))
Tactic:
simp [this]
Proof state after:
no goals
Theorem: RegularOpens.coe_top
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
⊢ ↑⊤ = univ
Tactic:
have : (⊤ : RegularOpens X) = (⊤ : Closeds X).int := rfl
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
this : ⊤ = Closeds.int ⊤
⊢ ↑⊤ = univ
Theorem: RegularOpens.coe_top
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
this : ⊤ = Closeds.int ⊤
⊢ ↑⊤ = univ
Tactic:
simp [this]
Proof state after:
no goals