rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm]
case h.e'_2
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 :
  ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i) =
    (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (ζ - 1) ^ ↑p * (algebraMap (𝓞 K) K) ((poly hp hζ u hcong).coeff i) =
    ((C ζ - 1) ^ ↑p * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i
case h.e'_2
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 :
  ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i) =
    (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (C ((ζ - 1) ^ ↑p) * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((C ζ - 1) ^ ↑p * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i