rw [← Ideal.mem_span_singleton, ← Ideal.Quotient.eq_zero_iff_mem, map_sub, this,
  map_sum]
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
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
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
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ∑ x_1 : K ≃ₐ[ℚ] K, (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((intGal ↑x_1).toRingHom x) -
      (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((↑p - 1) • x) =
    0