rw [← Int.gcd_eq_one_iff_coprime]
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ IsCoprime A B
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ Int.gcd A B = 1