Theorem: C05S03.primes_mod_4_eq_3_infinite (LeanCourse/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
⊢ ∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ p % 4 = 3
Tactic:
by_contra h
State after:
h : ¬∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ p % 4 = 3
⊢ False

State before:
h : ¬∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ p % 4 = 3
⊢ False
Tactic:
push_neg  at h
State after:
h : ∃ n, ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ False

State before:
h : ∃ n, ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ False
Tactic:
rcases h with ⟨n, hn⟩
State after:
case intro
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ False

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

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

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

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

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

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

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

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

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

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
State after:
no goals

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
State after:
case a
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ ∃ n, ∀ (k : ℕ), Nat.Prime k ∧ k % 4 = 3 → k ≤ n

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
State after:
case h
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
⊢ ∀ (k : ℕ), Nat.Prime k ∧ k % 4 = 3 → k ≤ n

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
State after:
case h
n : ℕ
hn : ∃ k, (Nat.Prime k ∧ k % 4 = 3) ∧ n < k
⊢ ∃ p > n, Nat.Prime p ∧ p % 4 = 3

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

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals