mathlib3

56f021a9 - feat(data/polynomial/{erase_lead + denoms_clearable}): strengthen a lemma (#11257)

feat(data/polynomial/{erase_lead + denoms_clearable}): strengthen a lemma (#11257) This PR is a step in the direction of simplifying #11139 . It strengthens lemma `induction_with_nat_degree_le` by showing that restriction can be strengthened on one of the assumptions. ~~It proves a lemma computing the `nat_degree` under functions on polynomials that include the shift of a variable.~~ EDIT: the lemma was moved to the later PR #11265. It fixes the unique use of lemma `induction_with_nat_degree_le`. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311139.20taylor.20sum.20and.20nat_degree_taylor)