apply is_principal_aux
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
case intro.hreg
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ p.Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))))

case intro.hI
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ span {↑a + ζ * ↑b} = ?intro.I ^ p

case intro.I
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))