rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
case h
n : ℕ
hn : ∃ k, (k.Prime ∧ k % 4 = 3) ∧ n < k
⊢ ∃ p > n, p.Prime ∧ p % 4 = 3
case h.intro.intro.intro
n p : ℕ
pltn : n < p
pp : p.Prime
p4 : p % 4 = 3
⊢ ∃ p > n, p.Prime ∧ p % 4 = 3