simp only [← hgcd, Finset.mem_singleton, Finset.mem_insert, neg_inj, Finset.gcd_insert, id_eq,
  ← Int.coe_gcd, Int.neg_gcd, Nat.cast_inj, ← insert_emptyc_eq, Finset.gcd_empty,
  Int.gcd_left_comm _ a]
case intro.intro.inl.inl.refine_1
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ {b, -c, -a}.gcd id = 1
no goals