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

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

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

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

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⟩
State after:
case intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
this : ∃ s, ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ False

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

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

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

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

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

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

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

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

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

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

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

State before:
case h
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ ∀ (k : ℕ), k.Prime ∧ k % 4 = 3 → k ≤ n
Tactic:
contrapose! hn
State after:
case h
n : ℕ
hn : ∃ k, (k.Prime ∧ k % 4 = 3) ∧ n < k
⊢ ∃ p > n, p.Prime ∧ p % 4 = 3

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : ℕ
⊢ n ∈ s.erase 3 → n.Prime
Tactic:
simp [← hs n]
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 = 3 → n.Prime → n % 4 = 3 → n.Prime

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 : ℕ
⊢ ¬n = 3 → n.Prime → n % 4 = 3 → n.Prime
Tactic:
tauto
State after:
no goals

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
pne3 : p ≠ 3
⊢ p ∣ 4 * ∏ i ∈ s.erase 3, i
Tactic:
apply dvd_trans _ (dvd_mul_left _ _)
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
pne3 : p ≠ 3
⊢ p ∣ ∏ i ∈ s.erase 3, i

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
pne3 : p ≠ 3
⊢ p ∣ ∏ i ∈ s.erase 3, i
Tactic:
apply dvd_prod_of_mem
State after:
case ha
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
⊢ p ∈ s.erase 3

State before:
case ha
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
⊢ p ∈ s.erase 3
Tactic:
simp
State after:
case ha
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
⊢ ¬p = 3 ∧ p ∈ s

State before:
case ha
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
⊢ ¬p = 3 ∧ p ∈ s
Tactic:
constructor <;> assumption
State after:
no goals

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
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i ∈ s.erase 3, i
⊢ p ∣ 3
Tactic:
convert Nat.dvd_sub' pdvd this
State after:
case h.e'_4
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
⊢ 3 = 4 * ∏ i ∈ s.erase 3, i + 3 - 4 * ∏ i ∈ s.erase 3, i

State before:
case h.e'_4
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
⊢ 3 = 4 * ∏ i ∈ s.erase 3, i + 3 - 4 * ∏ i ∈ s.erase 3, i
Tactic:
simp
State after:
no goals

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
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i ∈ s.erase 3, i
this : p ∣ 3
⊢ p = 3
Tactic:
apply pp.eq_of_dvd_of_prime Nat.prime_three this
State after:
no goals