Nat Weighted Degree coeffs To Poly le

lemma natWeightedDegree_coeffsToPoly_le (k D : ℕ) (c : (weigthBoundIndices k D) → F) :    natWeightedDegree (coeffsToPoly k D c) 1 (k - 1) ≤ D := by  have h_comb : ∃ (s : Finset (ℕ × ℕ)) (f : ℕ × ℕ → F), (coeffsToPoly k D c) =      ∑ p ∈ s, f p • (monomial (F := F) p.1 p.2) ∧ ∀ p ∈ s, p.1 + (k - 1) * p.2 ≤ D := by    norm_num +zetaDelta at *    refine ⟨univ.image      (fun p : { x // x ∈ weigthBoundIndices k D } ↦ (p.val.1, p.val.2)) , ?_, ?_ ⟩;    · use fun p ↦ if h : p ∈ univ.image          (fun p : { x // x ∈ weigthBoundIndices k D } ↦ (p.val.1, p.val.2))        then c ⟨p, by aesop⟩ else 0      unfold coeffsToPoly      simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,        linearCombination_apply, zero_smul, implies_true, sum_fintype, univ_eq_attach, Prod.mk.eta,        attach_image_val, dite_smul]      refine sum_bij (fun x hx ↦ x) ?_ ?_ ?_ ?_ <;> aesop    · unfold weigthBoundIndices at *; aesop  obtain ⟨s, f, h₁, h₂⟩ := h_comb  rw [h₁]  refine le_trans (natWeightedDegree_sum_le s _ _ _) ?_  refine Finset.sup_le fun p hp ↦ le_trans (natWeightedDegree_smul_le _ _ _ _) ?_  rw [natWeightedDegree_monomial_eq]  aesop