Fold Word k 1 of sq roots

theorem foldWord_k_1_of_sq_roots {i : Fin (2 ^ (n - 1))} {α : F}  {j j' : Fin (2 ^ n)} (hjj' : j ≠ j')  (hj : domain j ^ 2 = domain.subdomain 1 i) (hj' : domain j' ^ 2 = domain.subdomain 1 i) :  foldWord domain f 1 α i =    ((f j + f j') / 2) + α * ((f j - f j') / (2 * domain j)) := by  have hn : n ≠ 0 := by aesop (add safe [cases Fin, (by omega)])  letI : NeZero n := ⟨hn⟩  rw [foldWord_k_1]  extract_lets x a b  have ha : domain a = x := by simp [a]  have hb : domain b = -x := by simp [b]  have hx : x ^ 2 = domain.subdomain 1 i := by simp [x]  have hj_cases : domain j = x ∨ domain j = -x := by aesop (add safe eq_or_eq_neg_of_sq_eq_sq)  have hj'_cases : domain j' = x ∨ domain j' = -x := by aesop (add safe eq_or_eq_neg_of_sq_eq_sq)  rcases hj_cases with hjx | hjx <;> rcases hj'_cases with hj'x | hj'x <;>    try      exfalso      exact hjj' (CosetFftDomain.injective (hjx.trans hj'x.symm))  · obtain rfl : j = a := CosetFftDomain.injective (hjx.trans ha.symm)    obtain rfl : j' = b := CosetFftDomain.injective (hj'x.trans hb.symm)    rw [ha]  · obtain rfl : j = b := CosetFftDomain.injective (hjx.trans hb.symm)    obtain rfl : j' = a := CosetFftDomain.injective (hj'x.trans ha.symm)    rw [hb]    field_simp    ring