Mem fixed symm

theorem mem_fixed_symm (α κ : ℕ) (hκ : κ + 1 ≤ α) {e : ℕ} (hdvd : 2 ^ (α - κ - 1) ∣ e) :    Xpow (powTwoCyclotomic (R := R) α) e + conjAut α (Xpow (powTwoCyclotomic α) e)      ∈ fixedSubring α (2 ^ κ) := by  have hgenX : ∀ f, genAut α (2 ^ κ) (Xpow (powTwoCyclotomic (R := R) α) f)      = Xpow (powTwoCyclotomic α) (f * genExp (2 ^ κ)) := fun f => by    rw [genAut, galoisRingHom_apply, galoisAut_Xpow' α (genExp (2 ^ κ)) f (genExp_odd (2 ^ κ))]  have hpow : 4 * 2 ^ κ * 2 ^ (α - κ - 1) = 2 ^ (α + 1) := by    rw [show (4 : ℕ) = 2 ^ 2 from rfl, _root_.mul_assoc, ← pow_add, ← pow_add]; congr 1; omega  have h4ke : (2 : ℕ) ^ (α + 1) ∣ 4 * 2 ^ κ * e := by    obtain ⟨t, rfl⟩ := hdvd    exact ⟨t, by rw [← _root_.mul_assoc, hpow]⟩  have hconjsq : e * conjExp α * conjExp α ≡ e [MOD 2 ^ (α + 1)] := by    have hcsq : conjExp α * conjExp α ≡ 1 [MOD 2 ^ (α + 1)] := by      have hid : conjExp α * conjExp α = 2 ^ (α + 1) * (2 ^ (α + 1) - 2) + 1 := by        have hM2 : 2 ≤ 2 ^ (α + 1) := by          calc 2 = 2 ^ 1 := rfl            _ ≤ 2 ^ (α + 1) := Nat.pow_le_pow_right (by norm_num) (by omega)        obtain ⟨t, ht⟩ := Nat.exists_eq_add_of_le hM2        rw [conjExp, ht]        simp only [show 2 + t - 1 = t + 1 from by omega, show 2 + t - 2 = t from by omega]; ring      rw [Nat.ModEq, hid, Nat.mul_add_mod]    calc e * conjExp α * conjExp α = e * (conjExp α * conjExp α) := by ring      _ ≡ e * 1 [MOD 2 ^ (α + 1)] := Nat.ModEq.mul_left e hcsq      _ = e := _root_.mul_one e  have hgen : e * genExp (2 ^ κ) ≡ e [MOD 2 ^ (α + 1)] := by    have he : e * genExp (2 ^ κ) = e + 4 * 2 ^ κ * e := by rw [genExp]; ring    rw [he]    calc e + 4 * 2 ^ κ * e ≡ e + 0 [MOD 2 ^ (α + 1)] :=          Nat.ModEq.add_left e ((Nat.modEq_zero_iff_dvd).mpr h4ke)      _ = e := Nat.add_zero e  have hcgen : e * conjExp α * genExp (2 ^ κ) ≡ e * conjExp α [MOD 2 ^ (α + 1)] := by    have he : e * conjExp α * genExp (2 ^ κ) = e * conjExp α + 4 * 2 ^ κ * e * conjExp α := by      rw [genExp]; ring    rw [he]    calc e * conjExp α + 4 * 2 ^ κ * e * conjExp α ≡ e * conjExp α + 0 [MOD 2 ^ (α + 1)] :=          Nat.ModEq.add_left _ ((Nat.modEq_zero_iff_dvd).mpr (h4ke.mul_right _))      _ = e * conjExp α := Nat.add_zero _  rw [conjAut_Xpow, mem_fixedSubring_iff]  refine ⟨?_, ?_⟩  · rw [map_add, conjAut_Xpow, conjAut_Xpow, Xpow_congr_mod α hconjsq, _root_.add_comm]  · rw [map_add, hgenX, hgenX, Xpow_congr_mod α hgen, Xpow_congr_mod α hcgen]