exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Ha)
case refine'_3.inl.inl
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
Ha : a / d = 0
⊢ False
no goals