simp only [Int.cast_neg, Int.cast_mul, Int.cast_one, Int.cast_ofNat, neg_eq_zero,
  mul_eq_zero] at h
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑(-(c * 3)) = 0
⊢ ↑p ∣ c
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑p ∣ c