have hb : b ≠ 0 := fun hb => by simp [hb] at hprod
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
⊢ False
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
⊢ False