rw [← hu, mul_comm ((_ + ζ * _)), ← mul_assoc]
case mk.intro.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'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * α ^ p = ↑a + ζ * ↑b
case mk.intro.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'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * ↑u * (↑a + ζ * ↑b) = ↑a + ζ * ↑b