To Finset image to Fft Domain eq to Finset

@[simp]lemma toFinset_image_toFftDomain_eq_toFinset [Fintype ι] [DecidableEq F] {ω : D} :  Finset.image (fun (w : F) ↦ ω 0 * w) (toFftDomain ω).toFinset =    CosetFftDomainClass.toFinset ω := by  ext x  constructor <;> rintro h  · simp_all only [Finset.mem_image, mem_toFinset_iff_mem]    obtain ⟨a, h₁, h₂⟩ := h    rw [←h₂, mul_comm]    exact mul_mem_of_mem_toFftDomain_of_mem h₁ (by simp)  · simp_all only [mem_toFinset_iff_mem, Finset.mem_image]    obtain ⟨a, h⟩ := h    have : (ω 0)⁻¹ * x ∈ toFftDomain ω := by      rw [mem_toFftDomain_iff_mul_mem]      aesop    exists _, this    field_simp