Four pow i reindex

theorem four_pow_i_reindex (α κ i : ℕ) (hκ : κ + 1 ≤ α) :    ∑ a ∈ Finset.range (2 ^ (α - κ - 1)),        Xpow (powTwoCyclotomic (R := R) α) (i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)))      = Xpow (powTwoCyclotomic (R := R) α) i        * ∑ j ∈ Finset.range (2 ^ (α - κ - 1)),            (Xpow (powTwoCyclotomic (R := R) α) (4 * 2 ^ κ * i)) ^ j := by  have h2κ : 1 ≤ 2 ^ κ := Nat.one_le_two_pow  have hgM : (4 * 2 ^ κ : ℕ) ∣ 2 ^ (α + 1) := by    rw [show (4 * 2 ^ κ : ℕ) = 2 ^ (2 + κ) from by rw [show (4 : ℕ) = 2 ^ 2 from rfl, ← pow_add]]    exact pow_dvd_pow 2 (by omega)  have hMn : 4 * 2 ^ κ * 2 ^ (α - κ - 1) = 2 ^ (α + 1) := by    rw [show (4 : ℕ) = 2 ^ 2 from rfl, mul_assoc, ← pow_add, ← pow_add]; congr 1; omega  have hφinj : Set.InjOn (fun a => (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))      ↑(Finset.range (2 ^ (α - κ - 1))) := four_pow_injOn κ α hκ  have hψinj : Set.InjOn (fun j => 4 * 2 ^ κ * j + 1)      ↑(Finset.range (2 ^ (α - κ - 1))) := by    intro a _ b _ h    exact Nat.eq_of_mul_eq_mul_left (by positivity) (Nat.add_right_cancel h)  have himg : (Finset.range (2 ^ (α - κ - 1))).image        (fun a => (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))      = (Finset.range (2 ^ (α - κ - 1))).image (fun j => 4 * 2 ^ κ * j + 1) := by    apply Finset.eq_of_subset_of_card_le    · intro x hx      rw [Finset.mem_image] at hx ⊢      obtain ⟨a, _, rfl⟩ := hx      have hlt : (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) < 2 ^ (α + 1) := Nat.mod_lt _ (by positivity)      have hmod1 : (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) % (4 * 2 ^ κ) = 1 := by        rw [Nat.mod_mod_of_dvd _ hgM, Nat.pow_mod,          show (4 * 2 ^ κ + 1) % (4 * 2 ^ κ) = 1 from by            rw [Nat.add_mod_left]; exact Nat.mod_eq_of_lt (by omega),          one_pow, Nat.mod_eq_of_lt (by omega)]      have hge1 : 1 ≤ (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) := by        rcases Nat.eq_zero_or_pos ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) with h | h        · rw [h, Nat.zero_mod] at hmod1; exact absurd hmod1 (by norm_num)        · exact h      have hdvd : (4 * 2 ^ κ) ∣ ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) - 1) :=        (Nat.modEq_iff_dvd' hge1).mp (by rw [Nat.ModEq, hmod1, Nat.mod_eq_of_lt (by omega)])      refine ⟨((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) - 1) / (4 * 2 ^ κ), ?_, ?_⟩      · rw [Finset.mem_range]        have hbound : (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) - 1 < 4 * 2 ^ κ * 2 ^ (α - κ - 1) := by          rw [hMn]; omega        exact Nat.div_lt_of_lt_mul hbound      · rw [Nat.mul_div_cancel' hdvd]; omega    · rw [Finset.card_image_of_injOn hφinj, Finset.card_image_of_injOn hψinj]  have e1 : ∑ a ∈ Finset.range (2 ^ (α - κ - 1)),        Xpow (powTwoCyclotomic (R := R) α) (i * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)))      = ∑ x ∈ (Finset.range (2 ^ (α - κ - 1))).image          (fun a => (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)),          Xpow (powTwoCyclotomic (R := R) α) (i * x) :=    (Finset.sum_image (f := fun x => Xpow (powTwoCyclotomic (R := R) α) (i * x)) hφinj).symm  have e2 : ∑ x ∈ (Finset.range (2 ^ (α - κ - 1))).image (fun j => 4 * 2 ^ κ * j + 1),        Xpow (powTwoCyclotomic (R := R) α) (i * x)      = ∑ j ∈ Finset.range (2 ^ (α - κ - 1)),          Xpow (powTwoCyclotomic (R := R) α) (i * (4 * 2 ^ κ * j + 1)) :=    Finset.sum_image (f := fun x => Xpow (powTwoCyclotomic (R := R) α) (i * x)) hψinj  rw [e1, himg, e2, Finset.mul_sum]  refine Finset.sum_congr rfl (fun j _ => ?_)  rw [show i * (4 * 2 ^ κ * j + 1) = i + 4 * 2 ^ κ * i * j from by ring, Xpow_add, Xpow_mul]