rw [← Int.pow_dvd_pow_iff hn.ne', ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ∣ c
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ^ n ∣ ↑d ^ n * (A ^ n + B ^ n)