simp only [gcd_insert, id, gcd_singleton, normalize_apply, neg_mul]
case h.e'_2
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}
⊢ {a, -b, -c}.gcd id = {a, b, c}.gcd id
case h.e'_2
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}
⊢ GCDMonoid.gcd a (GCDMonoid.gcd (-b) (-(c * ↑(normUnit (-c))))) = GCDMonoid.gcd a (GCDMonoid.gcd b (c * ↑(normUnit c)))