rw [← hp]
case h
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ p ^ 2 = 2 * (d - 1) + 1
case h
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ 2 * d - 1 = 2 * (d - 1) + 1