exact
  ⟨A, B, C, HA', HB', HC',
    ⟨right_ne_zero_of_mul (by rwa [HA] at ha'), right_ne_zero_of_mul (by rwa [HB] at hb'),
      right_ne_zero_of_mul (by rwa [HC] at hc'), hsoln⟩,
    hcoprime, coprime_add_self_pow hn hsoln hcoprime,
    coprime_add_self_pow hn hsoln' hcoprime.symm⟩
case intro.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 = ↑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
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ∃ 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'
no goals