have hadiv : d ∣ a := gcd_dvd (by simp [s])
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
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
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
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0