rintro ⟨⟨p, hp⟩, ⟨q, hq⟩, ⟨r, hr⟩⟩
d : ℤ
⊢ ¬(IsSquare (2 * d - 1) ∧ IsSquare (5 * d - 1) ∧ IsSquare (d * 13 - 1))
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p * p
q : ℤ
hq : 5 * d - 1 = q * q
r : ℤ
hr : d * 13 - 1 = r * r
⊢ False