have hnat₁ : p ∣ n ^ 2 + 1 := by
  refine Int.natCast_dvd_natCast.mp ?_
  simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
  refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
  simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
  rw [pow_two, ← hy]; exact add_left_neg 1
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
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ∃ 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
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)