by_cases np : n.Prime
n : ℕ
h : n % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
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