obtain ⟨y, hy⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)