Trace H Xpow neg one sq

theorem traceH_Xpow_neg_one_sq (α k j : ℕ) (hk2pow : ∃ κ, k = 2 ^ κ) (hk : 2 * k ∣ 2 ^ α)    (hsq : Xpow (powTwoCyclotomic (R := R) α) (2 * j) = -1) :    traceH α k (Xpow (powTwoCyclotomic (R := R) α) j) = 0 := by  have hHlt : ∀ m, m ∈ Hexp α k → m < 2 ^ (α + 1) := by    intro m hmem    rw [Hexp, Finset.mem_biUnion] at hmem    obtain ⟨a, _, hma⟩ := hmem    rw [Finset.mem_insert, Finset.mem_singleton] at hma    rcases hma with rfl | rfl <;> exact Nat.mod_lt _ (by positivity)  have hmem : ∀ m, m ∈ Hexp α k → (conjExp α * m) % 2 ^ (α + 1) ∈ Hexp α k := by    intro m hm    rw [← Hexp_generator_smul α k (conjExp α) hk2pow hk (Or.inl rfl)]    exact Finset.mem_image_of_mem _ hm  rw [traceH_Xpow' α k j]  refine Finset.sum_involution (fun m _ => (conjExp α * m) % 2 ^ (α + 1)) ?_ ?_ hmem ?_  · intro m hm    have hmodd : Odd m := Hexp_odd_mem α k m hm    have hstep : Xpow (powTwoCyclotomic (R := R) α) (j * ((conjExp α * m) % 2 ^ (α + 1)))        = Xpow (powTwoCyclotomic (R := R) α) ((j * m) * conjExp α) := by      apply Xpow_congr_mod      exact calc j * ((conjExp α * m) % 2 ^ (α + 1))            ≡ j * (conjExp α * m) [MOD 2 ^ (α + 1)] := Nat.ModEq.mul_left _ (Nat.mod_modEq _ _)        _ = (j * m) * conjExp α := by ring    have hsqm : Xpow (powTwoCyclotomic (R := R) α) (2 * (j * m)) = -1 := by      rw [show 2 * (j * m) = (2 * j) * m from by ring, Xpow_mul, hsq, hmodd.neg_one_pow]    rw [hstep, Xpow_mul_conjExp α (j * m) hsqm, add_neg_cancel]  · intro m hm _ hgm    have hmodd : Odd m := Hexp_odd_mem α k m hm    have hmlt : m < 2 ^ (α + 1) := hHlt m hm    have hα : 1 ≤ α := by      obtain ⟨κ, rfl⟩ := hk2pow      have := succ_le_of_two_mul_two_pow_dvd hk; omega    have hcong : conjExp α * m ≡ m [MOD 2 ^ (α + 1)] := by      rw [Nat.ModEq, hgm, Nat.mod_eq_of_lt hmlt]    have hdvd : 2 ^ (α + 1) ∣ 2 * m := by      have e1 : conjExp α * m + m = 2 ^ (α + 1) * m := by        have hc : conjExp α + 1 = 2 ^ (α + 1) := by          have h1 : 1 ≤ 2 ^ (α + 1) := Nat.one_le_two_pow          rw [conjExp]; omega        calc conjExp α * m + m = (conjExp α + 1) * m := by ring          _ = 2 ^ (α + 1) * m := by rw [hc]      have h2m : 2 * m ≡ 0 [MOD 2 ^ (α + 1)] :=        calc 2 * m = m + m := by ring          _ ≡ conjExp α * m + m [MOD 2 ^ (α + 1)] := Nat.ModEq.add_right m hcong.symm          _ = 2 ^ (α + 1) * m := e1          _ ≡ 0 [MOD 2 ^ (α + 1)] := (Nat.modEq_zero_iff_dvd).mpr ⟨m, rfl⟩      exact (Nat.modEq_zero_iff_dvd).mp h2m    have hdvd2 : 2 ^ α ∣ m := by      have he : 2 ^ (α + 1) = 2 * 2 ^ α := by rw [pow_succ]; ring      rw [he] at hdvd      exact (Nat.mul_dvd_mul_iff_left (by norm_num : 0 < 2)).mp hdvd    have h2m : 2 ∣ m := dvd_trans (dvd_pow_self 2 (by omega : α ≠ 0)) hdvd2    obtain ⟨t, ht⟩ := hmodd    omega  · intro m hm    have hmlt : m < 2 ^ (α + 1) := hHlt m hm    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]    have key : conjExp α * ((conjExp α * m) % 2 ^ (α + 1)) ≡ m [MOD 2 ^ (α + 1)] :=      calc conjExp α * ((conjExp α * m) % 2 ^ (α + 1))            ≡ conjExp α * (conjExp α * m) [MOD 2 ^ (α + 1)] :=              Nat.ModEq.mul_left _ (Nat.mod_modEq _ _)        _ = (conjExp α * conjExp α) * m := by ring        _ ≡ 1 * m [MOD 2 ^ (α + 1)] := Nat.ModEq.mul_right m hcsq        _ = m := one_mul m    have heq : (conjExp α * ((conjExp α * m) % 2 ^ (α + 1))) % 2 ^ (α + 1) = m % 2 ^ (α + 1) := key    rw [heq, Nat.mod_eq_of_lt hmlt]