rcases Int.isUnit_iff.1 (normUnit (-c)).isUnit, Int.isUnit_iff.1 (normUnit c).isUnit with
  ⟨H₁ | H₂, H₃ | H₄⟩
case h.e'_2.e_a
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
case h.e'_2.e_a.inl.inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₁ : ↑(normUnit (-c)) = 1
H₃ : ↑(normUnit c) = 1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs

case h.e'_2.e_a.inl.inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₁ : ↑(normUnit (-c)) = 1
H₄ : ↑(normUnit c) = -1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs

case h.e'_2.e_a.inr.inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₂ : ↑(normUnit (-c)) = -1
H₃ : ↑(normUnit c) = 1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs

case h.e'_2.e_a.inr.inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₂ : ↑(normUnit (-c)) = -1
H₄ : ↑(normUnit c) = -1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs