replace 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 := by
    simp only [map_pow, map_sub, map_one, Polynomial.map_add, Polynomial.map_pow,
      Polynomial.map_sub, Polynomial.map_mul, map_C, IsPrimitiveRoot.coe_unit'_coe,
      Polynomial.map_one, map_X, coeff_add] at this
    convert this
    simp only [NumberField.RingOfIntegers.coe_eq_algebraMap, ← Polynomial.coeff_map]
    simp only [coeff_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_C,
      IsPrimitiveRoot.coe_unit'_coe, Polynomial.map_one]
    rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm]
    simp
case 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 :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (map (algebraMap (𝓞 K) K) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)).coeff i
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
case 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
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i