rw [← dvd_add_iff_left (dvd_mul_right _ _)] at H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2 + 3 * s ^ 2
⊢ 3 ∣ q
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2
⊢ 3 ∣ q