Galois Aut fixed of mem

theorem galoisAut_fixed_of_mem (α k : ℕ) {c : Rq (powTwoCyclotomic (R := R) α)}    (hc : c ∈ fixedSubring α k) :    ∀ m ∈ Hexp α k, galoisAut (powTwoCyclotomic α) m c = c := by  obtain ⟨hconjc, hgenc⟩ := (mem_fixedSubring_iff α k c).mp hc  have hodd1 : Odd (4 * k + 1) := ⟨2 * k, by ring⟩  have hgen' : galoisAut (powTwoCyclotomic α) (4 * k + 1) c = c := by    rw [genAut, galoisRingHom_apply] at hgenc; exact hgenc  have hconj' : galoisAut (powTwoCyclotomic α) (conjExp α) c = c := by    rw [conjAut, galoisRingHom_apply] at hconjc; exact hconjc  have hgen_pow : ∀ a, galoisAut (powTwoCyclotomic α) ((4 * k + 1) ^ a) c = c := by    intro a    induction a with    | zero => rw [pow_zero, galoisAut_one_eq]    | succ a ih =>      rw [pow_succ', ← galoisAut_comp α (4 * k + 1) ((4 * k + 1) ^ a) hodd1 hodd1.pow, ih, hgen']  have hmpos : 0 < 2 ^ (α + 1) := by positivity  have h2d : (2 : ℕ) ∣ 2 ^ (α + 1) := dvd_pow_self 2 (Nat.succ_ne_zero α)  intro m hm  rw [Hexp, Finset.mem_biUnion] at hm  obtain ⟨a, _, hma⟩ := hm  have hpa : (4 * k + 1) ^ a % 2 ^ (α + 1) < 2 ^ (α + 1) := Nat.mod_lt _ hmpos  have hpa_odd : Odd ((4 * k + 1) ^ a % 2 ^ (α + 1)) := by    rw [Nat.odd_iff, Nat.mod_mod_of_dvd _ h2d]; exact Nat.odd_iff.mp hodd1.pow  rw [Finset.mem_insert, Finset.mem_singleton] at hma  rcases hma with rfl | rfl  · rw [← galoisAut_periodic, hgen_pow]  · have hmodneg : (2 ^ (α + 1) - (4 * k + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1)        = (conjExp α * ((4 * k + 1) ^ a % 2 ^ (α + 1))) % 2 ^ (α + 1) := by      have hc1 : conjExp α + 1 = 2 ^ (α + 1) := by        rw [conjExp]; have : 1 ≤ 2 ^ (α + 1) := Nat.one_le_two_pow; omega      have hmodeq : conjExp α * ((4 * k + 1) ^ a % 2 ^ (α + 1))          ≡ 2 ^ (α + 1) - (4 * k + 1) ^ a % 2 ^ (α + 1) [MOD 2 ^ (α + 1)] := by        apply Nat.ModEq.add_right_cancel' ((4 * k + 1) ^ a % 2 ^ (α + 1))        rw [Nat.sub_add_cancel (le_of_lt hpa),          show conjExp α * ((4 * k + 1) ^ a % 2 ^ (α + 1)) + (4 * k + 1) ^ a % 2 ^ (α + 1)            = ((4 * k + 1) ^ a % 2 ^ (α + 1)) * 2 ^ (α + 1) from by            rw [conjExp, Nat.sub_mul, one_mul, mul_comm,              Nat.sub_add_cancel (Nat.le_mul_of_pos_right _ (by positivity))]]        exact (Nat.modEq_zero_iff_dvd.mpr ⟨(4 * k + 1) ^ a % 2 ^ (α + 1), mul_comm _ _⟩).trans          (Nat.modEq_zero_iff_dvd.mpr ⟨1, (mul_one _).symm⟩).symm      exact hmodeq.symm    rw [hmodneg, ← galoisAut_periodic,      ← galoisAut_comp α (conjExp α) ((4 * k + 1) ^ a % 2 ^ (α + 1)) (conjExp_odd α) hpa_odd,      ← galoisAut_periodic, hgen_pow, hconj']