simp only [← hI, submodule_span_eq, span_singleton_pow, span_singleton_eq_span_singleton] at hα
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : (fun J => J ^ p) I = (fun J => J ^ p) (Submodule.span (𝓞 K') {α})
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : Associated (↑a + ζ * ↑b) (α ^ p)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b