have hreal₂ : (p : ℝ) > 20 := by 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
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑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
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)