rw [smul_C, smul_eq_mul, ← smul_pow, ← mul_div_assoc, mul_div_cancel_left₀, smul_sub, smul_C,
  smul_eq_mul, mul_inv_cancel, map_one, Algebra.smul_def, ← C_eq_algebraMap, map_sub, map_one]
case a.a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
i : ℕ
this :
  (ζ - 1) ^ ↑p * ↑((poly hp hζ u hcong).coeff i) =
    (((C ((algebraMap (𝓞 K) K) ↑hζ.unit') - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i =
    ((ζ - 1) ^ ↑p • (X - C (ζ - 1)⁻¹) ^ ↑p).coeff i +
      ((ζ - 1) ^ ↑p • C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
case a.a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
i : ℕ
this :
  (ζ - 1) ^ ↑p * ↑((poly hp hζ u hcong).coeff i) =
    (((C ((algebraMap (𝓞 K) K) ↑hζ.unit') - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ ζ - 1 ≠ 0

case a.a.ha
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
i : ℕ
this :
  (ζ - 1) ^ ↑p * ↑((poly hp hζ u hcong).coeff i) =
    (((C ((algebraMap (𝓞 K) K) ↑hζ.unit') - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (ζ - 1) ^ ↑p ≠ 0