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

State before:
n : ℕ
h : n % 4 = 3
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases np : n.Prime
State after:
case pos
n : ℕ
h : n % 4 = 3
np : Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
h : n % 4 = 3
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg
n : ℕ
h : n % 4 = 3
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3
Tactic:
induction' n using Nat.strong_induction_on with n ih
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 : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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