Trace H psi mul conj

theorem traceH_psi_mul_conj (α k : ℕ) (h2 : (2 : R) ≠ 0) (hk2pow : ∃ κ, k = 2 ^ κ)    (hk : 2 * k ∣ 2 ^ α)    (a b : Fin (2 ^ α / k) → fixedSubring (R := R) α k) :    traceH α k (psi α k a * conjAut α (psi α k b))      = (2 ^ α / k) • ((∑ i, a i * b i : fixedSubring (R := R) α k) :          Rq (powTwoCyclotomic (R := R) α)) := by  obtain ⟨κ, rfl⟩ := hk2pow  have hκ : κ + 1 ≤ α := succ_le_of_two_mul_two_pow_dvd hk  -- `σ_{-1}(ψ(b)) = Σ_q ↑(b q)·X^{e_q·σ_{-1}}` (`σ_{-1}` fixes `b q ∈ R_q^H`)  have hconjpsi : conjAut α (psi α (2 ^ κ) b)      = ∑ q, (b q : Rq (powTwoCyclotomic α))          * Xpow (powTwoCyclotomic α) (packExp α (2 ^ κ) q.val * conjExp α) := by    unfold psi    rw [map_sum]    refine Finset.sum_congr rfl (fun q _ => ?_)    rw [map_mul, ((mem_fixedSubring_iff α (2 ^ κ) _).mp (b q).2).1, conjAut, galoisRingHom_apply,      galoisAut_Xpow' α (conjExp α) _ (conjExp_odd α)]  -- Rewrite each summand in place via `Finset.sum_congr`; the coefficient `↑(a p)·↑(b q)` arises  -- from `mul_mem`/`traceH_smul_fixed`, so it is never written as a `coe * coe` product (which  -- mis-resolves to the subring's `*`).  rw [hconjpsi]  unfold psi  rw [Finset.sum_mul_sum]  simp only [traceH_sum]  rw [Finset.sum_congr rfl (fun p _ => Finset.sum_congr rfl (fun q _ => by    rw [mul_mul_mul_comm, ← Xpow_add, traceH_smul_fixed α (2 ^ κ) (mul_mem (a p).2 (b q).2),      traceH_kernel α κ h2 hκ p q]))]  simp only [mul_ite, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, if_true, mul_smul_comm,    mul_one]  rw [← Finset.smul_sum]  congr 1  rw [AddSubmonoidClass.coe_finsetSum]  simp only [MulMemClass.coe_mul]