rw [← ZMod.intCast_eq_intCast_iff] at habs H
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : a ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
⊢ False
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ↑a = ↑b
habs : ↑a = ↑(-c)
hp3 : p ≠ 3
⊢ False