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

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

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

State before:
case neg
n : ℕ
h : n % 4 = 3
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
push_neg  at np
State after:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3

case neg.h.intro.intro.intro.inr
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h.intro.intro.intro.inr
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn
State after:
case neg.h.intro.intro.intro.inr.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.h.intro.intro.intro.inr.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases nmp : (n / m).Prime
State after:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : (n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬(n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬(n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases ih (n / m) nmltn h1 nmp with ⟨p, pp, pdvd, p4eq⟩
State after:
case neg.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬(n / m).Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

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

State before:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬(n / m).Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ n / m
p4eq : p % 4 = 3
⊢ p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
exact ⟨pp, pdvd.trans nmdvdn, p4eq⟩
State after:
no goals

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

State before:
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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 → ¬m.Prime → ∃ p, p.Prime ∧ 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, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases mp : m.Prime
State after:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases ih m mltn h1 mp with ⟨p, pp, pdvd, p4eq⟩
State after:
case neg.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case neg.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use p
State after:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ p.Prime ∧ p ∣ n ∧ p % 4 = 3

State before:
case h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
p4eq : p % 4 = 3
⊢ p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
exact ⟨pp, pdvd.trans mdvdn, p4eq⟩
State after:
no goals

State before:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use m
State after:
no goals

State before:
case pos
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ 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 : (n / m).Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
use n / m
State after:
no goals