Trace H Xpow eq zero

theorem traceH_Xpow_eq_zero (α k : ℕ) (h2 : (2 : R) ≠ 0) (hk2pow : ∃ κ, k = 2 ^ κ)    (hk : 2 * k ∣ 2 ^ α) {i : ℕ} (hi0 : ¬ (2 ^ α / (2 * k)) ∣ i) :    traceH α k (Xpow (powTwoCyclotomic (R := R) α) i) = 0 := by  obtain ⟨κ, rfl⟩ := hk2pow  have hκ : κ + 1 ≤ α := succ_le_of_two_mul_two_pow_dvd hk  have hrange : 2 ^ α / (2 * 2 ^ κ) = 2 ^ (α - κ - 1) := by    rw [show 2 * 2 ^ κ = 2 ^ (κ + 1) from by rw [pow_succ]; ring, Nat.pow_div hκ (by norm_num),      Nat.sub_sub]  have hi0' : ¬ 2 ^ (α - κ - 1) ∣ i := by rwa [hrange] at hi0  have hmpos : 0 < 2 ^ (α + 1) := by positivity  have hm4 : (4 : ℕ) ∣ 2 ^ (α + 1) := by    rw [show (4 : ℕ) = 2 ^ 2 from rfl]; exact pow_dvd_pow 2 (by omega)  have hm40 : 2 ^ (α + 1) % 4 = 0 := by obtain ⟨c, hc⟩ := hm4; omega  have hp4 : ∀ a, (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) % 4 = 1 := fun a => by    rw [Nat.mod_mod_of_dvd _ hm4, Nat.pow_mod]    norm_num [show (4 * 2 ^ κ + 1) % 4 = 1 from by omega]  have hplt : ∀ a, (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) < 2 ^ (α + 1) := fun a => Nat.mod_lt _ hmpos  have hqeq : ∀ a, (2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1)      = 2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) := fun a =>    Nat.mod_eq_of_lt (by have := hplt a; have := hp4 a; omega)  have hpinj : Set.InjOn (fun a => (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))      ↑(Finset.range (2 ^ (α - κ - 1))) := four_pow_injOn κ α hκ  -- the orbit sum and conjugate sum both vanish  have hTp : ∑ a ∈ Finset.range (2 ^ (α - κ - 1)),      Xpow (powTwoCyclotomic (R := R) α) (i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))) = 0 := by    rw [four_pow_i_reindex α κ i hκ, four_pow_i_geom_zero α κ i h2 hκ hi0', mul_zero]  have hTq : ∑ a ∈ Finset.range (2 ^ (α - κ - 1)),      Xpow (powTwoCyclotomic (R := R) α)        (i * ((2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1))) = 0 := by    have hconj : ∀ a ∈ Finset.range (2 ^ (α - κ - 1)),        Xpow (powTwoCyclotomic (R := R) α)          (i * ((2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1)))        = conjAut α (Xpow (powTwoCyclotomic (R := R) α)            (i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)))) := by      intro a _      rw [conjAut, galoisRingHom_apply, galoisAut_Xpow' α (conjExp α) _ (conjExp_odd α)]      apply Xpow_congr_mod      have hpa := hplt a      have key : i * (2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))          ≡ i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) * conjExp α [MOD 2 ^ (α + 1)] := by        apply Nat.ModEq.add_right_cancel' (i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)))        have hc1 : conjExp α + 1 = 2 ^ (α + 1) := by          rw [conjExp]; have : 1 ≤ 2 ^ (α + 1) := Nat.one_le_two_pow; omega        rw [← Nat.mul_add,          Nat.sub_add_cancel (le_of_lt hpa),          show i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) * conjExp α              + i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))            = i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) * 2 ^ (α + 1) from by            rw [← hc1]; ring]        exact (Nat.modEq_zero_iff_dvd.mpr ⟨i, by ring⟩).trans          (Nat.modEq_zero_iff_dvd.mpr ⟨i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)), by ring⟩).symm      exact (Nat.ModEq.mul_left i (Nat.mod_modEq _ _)).trans key    rw [Finset.sum_congr rfl hconj, ← map_sum, hTp, map_zero]  -- assemble  rw [traceH_Xpow' α (2 ^ κ)]  unfold Hexp  rw [hrange, Finset.sum_biUnion (by    intro a ha b hb hab    simp only [Function.onFun]    rw [Finset.disjoint_left]    have hpab : (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) ≠ (4 * 2 ^ κ + 1) ^ b % 2 ^ (α + 1) :=      fun h => hab (hpinj ha hb h)    intro x hx hx'    rw [hqeq a] at hx; rw [hqeq b] at hx'    simp only [Finset.mem_insert, Finset.mem_singleton] at hx hx'    have := hp4 a; have := hp4 b; have := hplt a; have := hplt b    rcases hx with rfl | rfl <;> rcases hx' with h' | h' <;> omega)]  rw [Finset.sum_congr rfl (fun a _ => Finset.sum_pair (by    rw [hqeq a]; have := hp4 a; have := hplt a; omega)),    Finset.sum_add_distrib, hTp, hTq, add_zero]