have : m % 4 = 3 ∨ n / m % 4 = 3 := by
  apply mod_4_eq_3_or_mod_4_eq_3
  rw [neq, h]
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
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