mathlib3

c81c6c91 - feat(data/polynomial/erase_lead): `lt_nat_degree_of_mem_erase_lead_support` (#14745)

feat(data/polynomial/erase_lead): `lt_nat_degree_of_mem_erase_lead_support` (#14745) This PR adds a lemma `lt_nat_degree_of_mem_erase_lead_support` and adds term-mode proofs of a couple related lemmas.