Pow Contraction is right inverse to linear Mv Extension

lemma powContraction_is_right_inverse_to_linearMvExtension    (p : Polynomial.degreeLT F (2 ^ m)) :    powContraction.comp linearMvExtensionLMap p = p := by  have hnat : (p : Polynomial F).natDegree < 2 ^ m := by    have hdeg := Polynomial.mem_degreeLT.mp p.2    by_cases hp : (p : Polynomial F) = 0    · simp [hp]    · exact (Polynomial.natDegree_lt_iff_degree_lt hp).mpr hdeg  have h_comp : powContraction (linearMvExtensionLMap p) =      ∑ i ∈ Finset.range (2 ^ m), p.val.coeff i • Polynomial.X ^ i := by    unfold powContraction linearMvExtensionLMap linearMvExtension    simp +decide only [LinearMap.coe_mk, AddHom.coe_mk, AlgHom.toLinearMap_apply, powAlgHom]    rw [MvPolynomial.aeval_def]    have h_sum_range :        (p : Polynomial F).sum (fun i a => MvPolynomial.monomial (bitExpo (m := m) i) a) =          ∑ i ∈ Finset.range (2 ^ m),            MvPolynomial.monomial (bitExpo (m := m) i) ((p : Polynomial F).coeff i) := by      exact Polynomial.sum_over_range' (p : Polynomial F) (by intro n; simp) (2 ^ m) hnat    rw [h_sum_range, MvPolynomial.eval₂_sum]    refine Finset.sum_congr rfl ?_    intro i hi    simp +decide only [Polynomial.algebraMap_eq, eval₂_monomial, Finsupp.prod_pow]    have h_sum : ∑ x : Fin m, 2 ^ (x : ℕ) * (bitExpo i) x = i := by      convert binary_repr_sum m i (Finset.mem_range.mp hi) using 1      rw [Finset.sum_range]      unfold bitExpo; aesop    simp_rw [← pow_mul]    rw [Finset.prod_pow_eq_pow_sum, h_sum]    simp [Polynomial.smul_eq_C_mul]  change powContraction (linearMvExtensionLMap p) = (p : Polynomial F)  rw [h_comp]  convert (Polynomial.as_sum_range' p.val (2 ^ m) hnat).symm using 1  simp +decide [Polynomial.smul_eq_C_mul, ← Polynomial.C_mul_X_pow_eq_monomial]