English
For any p in MvPolynomial(Option S1) and any i, the total degree of the i-th coefficient of optionEquivLeft(R,S1)(p) plus i does not exceed the total degree of p, provided i is within p.totalDegree.
Русский
Для любого p ∈ MvPolynomial(Option S1) и любого i, общая скорость i-й коэффициентной части optionEquivLeft(R,S1)(p) плюс i не превосходит totalDegree p, при условии i ≤ p.totalDegree.
LaTeX
$$$\\text{If } i \\le p.totalDegree, \\; \\operatorname{totalDegree}(((\\operatorname{optionEquivLeft} R S_1\\;p).\\coeff i)) + i \\le p.totalDegree.$$$
Lean4
theorem totalDegree_coeff_optionEquivLeft_add_le (p : MvPolynomial (Option S₁) R) (i : ℕ) (hi : i ≤ p.totalDegree) :
((optionEquivLeft R S₁ p).coeff i).totalDegree + i ≤ p.totalDegree := by
classical
by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
· rw [hpi]; simpa
rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
intro σ hσ
refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
· simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
· simpa [mem_support_iff, ← optionEquivLeft_coeff_coeff R S₁] using hσ
