Subdomain to Fft Domain comm

lemma subdomain_toFftDomain_comm {i : ℕ} :  (subdomain ω i).toFftDomain = FftDomainClass.subdomain (toFftDomain ω) i := by  ext u  rw [eval_toFftDomain]  conv_rhs =>    simp [FftDomainClass.subdomain]  rw [eval_toFftDomain]  conv_rhs =>    rw [CosetFftDomain.map_0_eq_coset_generator]  rw [subdomain_generator_pow_generator]  simp only [FftDomainClass.apply_zero_eq_one, one_pow, inv_one, one_mul]  conv_rhs =>    simp [subdomain]    rw [CosetFftDomain.eval_coset_fft_domain_eq_eval_generator_mul_domain]    simp [CosetFftDomainClass.subdomain_embed, mkSubgroupUnit]  by_cases h : n ≤ i  · obtain ⟨u, hu⟩ := u    have : n - i = 0 := by omega    simp [this] at hu    aesop  · simp only [h, ↓reduceDIte]    rw [CosetFftDomainClass.eval_toFftDomain]    conv_lhs =>      rhs      simp only [        subdomain, mkSubgroupUnit,        CosetFftDomainClass.subdomain_embed,        ge_iff_le, inv_pow,        CosetFftDomain.eval_coset_fft_domain_eq_eval_generator_mul_domain,        h, ↓reduceDIte, MonoidHom.coe_mk, OneHom.coe_mk]    rw [CosetFftDomain.map_0_eq_coset_generator,        CosetFftDomainClass.subdomain_generator_pow_generator]    simp