simp [dvd_gcd_iff, hz, hy, this]
case intro.intro.intro.intro.intro.intro
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✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
hy : ↑p ∣ y
this : ↑p ∣ x
⊢ ↑p ∣ {x, y, z}.gcd id
no goals