Mem rs code iff exists mle

lemma mem_rs_code_iff_exists_mle  {f : ι → F} {deg : ℕ} :  f ∈ code domain (2 ^ deg) ↔    ∃ g : F⦃≤ 1⦄[X (Fin deg)], f = evalOnPoints domain (powAlgHom g.1) := by  constructor <;> intro h  · rw [mem_code_iff_exists_polynomial] at h    obtain ⟨g, hdeg, h⟩ := h    let poly := linearMvExtension (m := deg) ⟨g, by      aesop (add simp [Polynomial.mem_degreeLT])    ⟩    exists ⟨poly, by aesop (add simp [mem_restrictDegree_iff_degreeOf_le,                                       linearMvExtension_degreeOf_lt])⟩    aesop (add simp powAlgHom_is_right_inverse_to_linearMvExtension)  · obtain ⟨g, h⟩ := h    exact mem_code_of_polynomial_of_natDegree_lt_of_eval      (powAlgHom g.1)      (lt_of_le_of_lt powAlgHom_of_restrict_degree_natDegree (by grind))      (by aesop)