simp only [mul_eq_zero] at habs
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : a / d * (b / d) * (c / d) = 0
⊢ False
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : (a / d = 0 ∨ b / d = 0) ∨ c / d = 0
⊢ False