Four pow i geom zero

theorem four_pow_i_geom_zero (α κ i : ℕ) (h2 : (2 : R) ≠ 0) (hκ : κ + 1 ≤ α)    (hi0 : ¬ 2 ^ (α - κ - 1) ∣ i) :    ∑ j ∈ Finset.range (2 ^ (α - κ - 1)),      (Xpow (powTwoCyclotomic (R := R) α) (4 * 2 ^ κ * i)) ^ j = 0 := by  apply geom_sum_eq_zero_of_isUnit  · rw [← Xpow_mul]    have he : 4 * 2 ^ κ * i * 2 ^ (α - κ - 1) = 2 ^ (α + 1) * i := by      have h4 : (4 : ℕ) * 2 ^ κ * 2 ^ (α - κ - 1) = 2 ^ (α + 1) := by        rw [show (4 : ℕ) = 2 ^ 2 from rfl, mul_assoc, ← pow_add, ← pow_add]; congr 1; omega      calc 4 * 2 ^ κ * i * 2 ^ (α - κ - 1) = (4 * 2 ^ κ * 2 ^ (α - κ - 1)) * i := by ring        _ = 2 ^ (α + 1) * i := by rw [h4]    rw [he, Xpow_mul, Xpow_conductor, one_pow]  · have hine : i ≠ 0 := by rintro rfl; exact hi0 (dvd_zero _)    have hα2 : κ + 2 ≤ α := by      rcases Nat.lt_or_ge α (κ + 2) with h | h      · exact absurd (show 2 ^ (α - κ - 1) ∣ i from by          rw [show α - κ - 1 = 0 from by omega, pow_zero]; exact one_dvd i) hi0      · exact h    obtain ⟨w, i', hi'odd, hieq⟩ := Nat.exists_eq_two_pow_mul_odd hine    have hw : w ≤ α - κ - 2 := by      by_contra hge      exact hi0 (hieq ▸ Dvd.dvd.mul_right (pow_dvd_pow 2 (by omega : α - κ - 1 ≤ w)) i')    apply Xpow_sub_one_isUnit α h2 (t := α - κ - 2 - w)    have he2 : 4 * 2 ^ κ * i * 2 ^ (α - κ - 2 - w) = 2 ^ α * i' := by      rw [hieq, show 4 * 2 ^ κ * (2 ^ w * i') * 2 ^ (α - κ - 2 - w)          = (4 * 2 ^ κ * 2 ^ w * 2 ^ (α - κ - 2 - w)) * i' from by ring]      congr 1      rw [show (4 : ℕ) = 2 ^ 2 from rfl, ← pow_add, ← pow_add, ← pow_add]; congr 1; omega    rw [he2, Xpow_mul, Xpow_natDegree, hi'odd.neg_one_pow]