rw [hζ.subOneIntegralPowerBasis'_gen]
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.subOneIntegralPowerBasis'.gen
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.toInteger - 1