rw [hx]
case this
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
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ✝.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : 𝓞 K
hx : ↑(u ^ (↑p - 1)) - 1 = ↑↑p * x
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑(u ^ (↑p - 1)) - 1
case this
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
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ✝.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L : Type ?u.56521
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : ∃ n, ↑↑p ∣ ↑u - ↑n
this : Fact (↑p).Prime
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : 𝓞 K
hx : ↑(u ^ (↑p - 1)) - 1 = ↑↑p * x
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * x