Mk reverse eq galois Autₛ mul

theorem mk_reverse_eq_galoisAutₛ_mul (α : ℕ) (p : (ZMod q)[X]) :    Ideal.Quotient.mk (powTwoCyclotomic (R := ZMod q) α).modIdeal p.reverse      = galoisAutₛ α (conjExp α) (conjExp_odd α)          (Ideal.Quotient.mk (powTwoCyclotomic (R := ZMod q) α).modIdeal p)        * (Ideal.Quotient.mk (powTwoCyclotomic (R := ZMod q) α).modIdeal X) ^ p.natDegree := by  set mk := Ideal.Quotient.mk (powTwoCyclotomic (R := ZMod q) α).modIdeal with hmkdef  set x : (powTwoCyclotomic (R := ZMod q) α).CyclotomicRing := mk X with hxdef  have hx2d : x ^ (2 ^ (α + 1)) = 1 := by rw [hxdef, ← map_pow]; exact mk_X_pow_conductor_eq_one α  have hcx : x ^ (conjExp α) * x = 1 := by    rw [← pow_succ, conjExp, Nat.sub_add_cancel Nat.one_le_two_pow, hx2d]  letI invx : Invertible x := ⟨x ^ (conjExp α), hcx, by rw [mul_comm]; exact hcx⟩  set i : ZMod q →+* (powTwoCyclotomic (R := ZMod q) α).CyclotomicRing := mk.comp C with hidef  have heval_mk : ∀ r : (ZMod q)[X], eval₂ i x r = mk r := by    have hext : (Polynomial.eval₂RingHom i x) = mk := by      apply Polynomial.ringHom_ext      · intro a        simp only [Polynomial.coe_eval₂RingHom, eval₂_C, hidef, RingHom.comp_apply]      · simp only [Polynomial.coe_eval₂RingHom, eval₂_X, hxdef]    intro r; rw [← hext]; rfl  have hxc : mk (X ^ (conjExp α)) = ⅟x := by rw [map_pow]; rfl  have hsigma : galoisAutₛ α (conjExp α) (conjExp_odd α) (mk p) = eval₂ i (⅟x) p := by    rw [galoisAutₛ_mk, Polynomial.aeval_def, Polynomial.algebraMap_eq, Polynomial.hom_eval₂,      ← hidef, hxc]  have hrev := Polynomial.eval₂_reverse_mul_pow i (⅟x) p  rw [invOf_invOf, heval_mk, ← hsigma] at hrev  rw [← hrev, mul_assoc, ← mul_pow, invOf_mul_self, one_pow, mul_one]