have hnat₅ : p ∣ k ^ 2 + 4 := by
  cases' hnat₁ with x hx
  have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
    use (p : ℤ) - 4 * n + 4 * x
    have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast
    have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
    linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
  assumption_mod_cast
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
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
⊢ ∃ 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
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)