Xpow mul coeff

theorem Xpow_mul_coeff (α e : ℕ) (he : e < 2 ^ α) (x : Rq (powTwoCyclotomic (R := R) α))    {p : ℕ} (hp : p < 2 ^ α) :    (x * Xpow (powTwoCyclotomic α) e).1.coeff p      = if e ≤ p then x.1.coeff (p - e) else - x.1.coeff (p + 2 ^ α - e) := by  have hexp : x = ∑ k ∈ Finset.range (2 ^ α),      Rq.mk (powTwoCyclotomic α) (CompPoly.CPolynomial.monomial k (x.1.coeff k)) := by    conv_lhs => rw [← galoisAut_one_eq α x]    rw [galoisAut_eq_sum]    simp only [_root_.mul_one, powTwoCyclotomic_natDegree]  conv_lhs => rw [hexp, Finset.sum_mul, ← Rq.coeffHom_apply, map_sum]  simp only [Rq.coeffHom_apply, mk_monomial_mul_Xpow, mk_monomial_coeff_full]  by_cases hep : e ≤ p  · rw [if_pos hep, Finset.sum_eq_single (p - e)]    · have h1 : p - e + e = p := by omega      rw [h1, Nat.mod_eq_of_lt hp, Nat.div_eq_of_lt hp, pow_zero, _root_.one_mul, if_pos rfl]    · intro k hk hkne      rw [Finset.mem_range] at hk      rw [if_neg]      intro hpk      rcases lt_or_ge (k + e) (2 ^ α) with hlt | hge      · rw [Nat.mod_eq_of_lt hlt] at hpk; exact hkne (by omega)      · rw [Nat.mod_eq_sub_mod hge, Nat.mod_eq_of_lt (by omega)] at hpk; omega    · intro h; exact absurd (Finset.mem_range.mpr (by omega : p - e < 2 ^ α)) h  · rw [if_neg hep, Finset.sum_eq_single (p + 2 ^ α - e)]    · have h1 : p + 2 ^ α - e + e = p + 2 ^ α := by omega      rw [h1, Nat.add_mod_right, Nat.mod_eq_of_lt hp, Nat.add_div_right _ (by positivity),        Nat.div_eq_of_lt hp, _root_.zero_add, pow_one, neg_one_mul, if_pos rfl]    · intro k hk hkne      rw [Finset.mem_range] at hk      rw [if_neg]      intro hpk      rcases lt_or_ge (k + e) (2 ^ α) with hlt | hge      · rw [Nat.mod_eq_of_lt hlt] at hpk; omega      · rw [Nat.mod_eq_sub_mod hge, Nat.mod_eq_of_lt (by omega)] at hpk; exact hkne (by omega)    · intro h; exact absurd (Finset.mem_range.mpr (by omega : p + 2 ^ α - e < 2 ^ α)) h