Pow mem of mem

theorem pow_mem_of_mem {i j : ℕ} (hsum : j + i ≤ n) (h : x ∈ subdomain ω j) :  x ^ 2 ^ i ∈ subdomain ω (j + i) := by  obtain ⟨k, hk⟩ :    ∃ k : Fin (2 ^ (n - j)), x =      (mkSubgroupUnit ω (CosetFftDomainClass.subdomain_embed j k) : F) * (ω 0) ^ 2 ^ j := by    obtain ⟨k, rfl⟩ := h    exact ⟨k, mul_comm _ _⟩  have hx_pow :    x ^ 2 ^ i =      ((ω 0) ^ 2 ^ (j + i)) *        (mkSubgroupUnit ω (2 ^ i • CosetFftDomainClass.subdomain_embed j k) : F) := by    convert congr_arg (· ^ 2 ^ i) hk using 1    ring_nf    simp [←mkSubgroupUnit_pow]  have h_mod :    (2 ^ i • CosetFftDomainClass.subdomain_embed j k).val =      (2 ^ (j + i) *        (k.val % 2 ^ (n - (j + i)))) % 2 ^ n := by    have h_mod :      (2 ^ i • CosetFftDomainClass.subdomain_embed j k).val =        (2 ^ i *          (CosetFftDomainClass.subdomain_embed j k).val) % 2 ^ n := by      convert fin_nsmul_val _ _    by_cases hj : j < n    · simp_all only [CosetFftDomainClass.subdomain_embed, ge_iff_le, smul_dite, nsmul_zero]      split_ifs      · simp_all only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, mul_zero]        linarith      · simp_all only [↓reduceDIte, pow_add, mul_assoc]        convert nat_mul_pow_mod (show j + i ≤ n from hsum) using 1        ring_nf    · have : n = j := by linarith      aesop        (add simp [CosetFftDomainClass.subdomain_embed, Nat.mod_one])  have h_subdomain :    (CosetFftDomainClass.subdomain_embed      (n := n) (j + i) ⟨k.val % 2 ^ (n - (j + i)),    Nat.mod_lt _ (by positivity)⟩).val =    2 ^ (j + i) * (k.val % 2 ^ (n - (j + i))) := by    by_cases hi : j + i ≥ n      <;> aesop            (add simp [CosetFftDomainClass.subdomain_embed, Nat.mod_one])            (add safe (by grind))  generalize_proofs at *  have h_eq :    2 ^ i • CosetFftDomainClass.subdomain_embed j k =      CosetFftDomainClass.subdomain_embed        (j + i) ⟨k.val % 2 ^ (n - (j + i)), by assumption⟩ := Fin.ext <| by      simpa [Nat.mod_eq_of_lt (show 2 ^ (j + i) * (k.val % 2 ^ (n - (j + i))) <        2 ^ n from lt_of_lt_of_le          (Nat.mul_lt_mul_of_pos_left ‹_› (pow_pos (by decide) _))          (by rw [← pow_add, Nat.add_sub_of_le hsum]))]      using h_mod.trans <| h_subdomain.symm ▸        Nat.mod_eq_of_lt          (show 2 ^ (j + i) * (k.val % 2 ^ (n - (j + i))) < 2 ^ n from            lt_of_lt_of_le              (Nat.mul_lt_mul_of_pos_left ‹_› (pow_pos (by decide) _))              (by rw [← pow_add, Nat.add_sub_of_le hsum]))  generalize_proofs at *  use Multiplicative.ofAdd ⟨k.val % 2 ^ (n - (j + i)), by assumption⟩  generalize_proofs at *  convert hx_pow.symm using 1  exact Eq.symm    (Mathlib.Tactic.CancelDenoms.derive_trans₂      rfl (congrArg Units.val (congrArg (mkSubgroupUnit ω) h_eq)) rfl)