have hdp : d  = 2*(k + k^2) + 1 := by
  rw [hk, ←(add_left_inj 1), sub_add_cancel _] at hp
  ring_nf at hp
  have h422 : (4 : ℤ) = 2 * 2 := by norm_num
  simp only [h422,  ← mul_assoc] at hp
  nth_rw 1 [← one_mul 2] at hp
  rw [← add_mul, ← add_mul, mul_left_inj' two_ne_zero] at hp
  rw [← hp]
  ring
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
⊢ False
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
⊢ False