obtain ⟨B, HB⟩ : ↑d ∣ b := Int.gcd_dvd_right a b
case intro
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 = ?m.1006 * A
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
case intro.intro
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 = ?m.1006 * A
B : ℤ
HB : b = ?m.1144 * B
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'