Card block of mem subdomain

lemma card_block_of_mem_subdomain [DecidableEq F]  {i j : ℕ} (hij : i + j ≤ n) (h : x ∈ subdomain ω (i + j)) :  Finset.card (block (subdomain ω i) j x) = 2 ^ j := by  have hinj : Function.Injective (subdomain ω i) := CosetFftDomainClass.injective _  unfold block  obtain ⟨m, hm⟩ := h  have hinj2 : Function.Injective (subdomain ω (i + j)) := CosetFftDomainClass.injective _  have hfilter_eq : (Finset.univ.filter (fun k : Fin (2 ^ (n - i)) =>      ((subdomain ω i) k) ^ 2 ^ j = x)) =        Finset.univ.filter (fun k : Fin (2 ^ (n - i)) =>        k.val % 2 ^ (n - (i + j)) = m.val) := by    ext k    simp only [Finset.mem_filter, Finset.mem_univ, true_and]    rw [subdomain_eval_pow' hij k, ← hm]    constructor    · intro heq      have := hinj2 heq      simp only [Fin.ext_iff] at this      exact this    · intro heq      congr 1      exact Fin.ext heq  have :    {y ∈ toFinset (subdomain ω i) | y ^ 2 ^ j = x} =      Finset.image (subdomain ω i) (Finset.univ.filter (fun k : Fin (2 ^ (n - i)) =>      ((subdomain ω i) k) ^ 2 ^ j = x)) := by    ext u    simp    aesop (add simp [mem_def])  rw [this, Finset.card_image_of_injective _ hinj, hfilter_eq]  simp only [show n - (i + j) = n - i - j from by omega]  have hsub : n - (i + j) = n - i - j := by omega  exact card_fin_filter_mod_eq (by omega) m.val (hsub ▸ m.isLt)