Fix First Variables Of MQP degree Var LE

theorem fixFirstVariablesOfMQP_degreeVarLE    {b : Fin ℓ → ℕ} (v : Fin (ℓ + 1)) {challenges : Fin v → L}    {poly : MvPolynomial (Fin ℓ) L}    (hp : poly ∈ restrictDegreeVar (Fin ℓ) L b) :    fixFirstVariablesOfMQP ℓ v poly challenges ∈      restrictDegreeVar (Fin (ℓ - v)) L (b ∘ fixFirstVariablesOfMQP_survivingIndex ℓ v) := by  rw [MvPolynomial.mem_restrictDegreeVar]  unfold fixFirstVariablesOfMQP  dsimp only  intro term h_term_in_support i  have h_l_eq : ℓ = v + (ℓ - v) := (Nat.add_sub_of_le v.is_le).symm  set finEquiv := (finSumFinEquiv (m := v) (n := ℓ - v)).symm.trans (Equiv.sumComm _ _)  set e : Fin ℓ ≃ Fin (ℓ - v) ⊕ Fin v := (finCongr h_l_eq).trans finEquiv with he  set H_sum := MvPolynomial.rename (f := e) poly  set H_grouped : L[X Fin ↑v][X Fin (ℓ - ↑v)] := (sumAlgEquiv L (Fin (ℓ - v)) (Fin v)) H_sum  set eval_map : L[X Fin ↑v] →+* L := (eval challenges : MvPolynomial (Fin v) L →+* L)  have h_Hgrouped_degreeVarLE :      H_grouped ∈ restrictDegreeVar (Fin (ℓ - v)) (L[X Fin ↑v]) ((b ∘ e.symm) ∘ Sum.inl) :=    sumAlgEquiv_mem_restrictDegreeVar H_sum      (rename_equiv_mem_restrictDegreeVar e poly hp)  have h_term_in_Hgrouped_support : term ∈ H_grouped.support :=    MvPolynomial.support_map_subset _ _ h_term_in_support  have h_bound : term i ≤ (b ∘ e.symm) (Sum.inl i) :=    (MvPolynomial.mem_restrictDegreeVar H_grouped).mp h_Hgrouped_degreeVarLE      term h_term_in_Hgrouped_support i  -- Bound-equality: (b ∘ e.symm) (Sum.inl i) is the original suffix variable `v + i`.  have h_eq : e.symm (Sum.inl i) = fixFirstVariablesOfMQP_survivingIndex ℓ v i := by    apply Fin.ext    simp [he, finEquiv, fixFirstVariablesOfMQP_survivingIndex]  change term i ≤ b (fixFirstVariablesOfMQP_survivingIndex ℓ v i)  rw [← h_eq]  exact h_bound