haveI := Fact.mk hpp
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)