obtain ⟨nb, hnb⟩ := hbdiv
case refine'_1.intro
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
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
case refine'_1.intro.intro
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
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n