Neg one mem domain

@[simp]lemma neg_one_mem_domain [nz : NeZero n] :  -1 ∈ ω := by  have hn : n ≠ 0 := NeZero.ne _  -- Let's denote this element as `k = 2^(i-1) : Fin (2^i)`.  set k : Fin (2 ^ n) := ⟨2 ^ (n - 1), pow_lt_pow_right₀ (by decide) (by omega)⟩  generalize_proofs at *  have h_order : (ω k) ^ 2 = 1 := by    have hk_order : (ω k) ^ 2 = (ω (k + k)) := by aesop (add simp [sq, apply_add_eq_mul])    convert hk_order using 1    rw [show k + k = 0 by {      rcases n with ⟨_ | n, hn⟩        <;> norm_num [Fin.ext_iff, Fin.val_add, Fin.val_mul] at *      ring_nf at *      aesop    }]    aesop  generalize_proofs at *  (  -- Since $k$ has additive order 2 in $\text{Fin}(2^i)$, we have $(ω.subdomain i k) \neq 1$.  have h_ne_one : (ω k) ≠ 1 := by    have h_ne_one : (ω k) ≠ ω 0 := by      exact fun h ↦        absurd          (CosetFftDomainClass.injective _ h)          (ne_of_gt <| Nat.lt_of_le_of_lt (Nat.zero_le _) <| pow_pos (by omega) _)    generalize_proofs at *    (    exact fun h ↦ h_ne_one <| h.trans <| by simp )  generalize_proofs at *  (exact ⟨k, Or.resolve_left (sq_eq_one_iff.mp h_order) h_ne_one⟩))