refine' ⟨_, _, fun habs => _⟩
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
⊢ 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
case refine'_1
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
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n

case refine'_2
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
⊢ {a / d, b / d, c / d}.gcd id = 1

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