feat(data/polynomial/{erase_lead + denoms_clearable}): strengthen a l…

…emma (#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)

src/data/polynomial/denoms_clearable.lean

@@ -60,10 +60,10 @@ lemma denoms_clearable.add {N : ℕ} {f g : polynomial R} :
 
 lemma denoms_clearable_of_nat_degree_le (N : ℕ) (a : R) (bu : bi * i b = 1) :
   ∀ (f : polynomial R), f.nat_degree ≤ N → denoms_clearable a b N f i :=
-induction_with_nat_degree_le N
+induction_with_nat_degree_le _ N
   (denoms_clearable_zero N a bu)
   (λ N_1 r r0, denoms_clearable_C_mul_X_pow a bu r)
-  (λ f g fN gN df dg, df.add dg)
+  (λ f g fg gN df dg, df.add dg)
 
 /-- If `i : R → K` is a ring homomorphism, `f` is a polynomial with coefficients in `R`,
 `a, b` are elements of `R`, with `i b` invertible, then there is a `D ∈ R` such that

src/data/polynomial/erase_lead.lean

@@ -160,10 +160,11 @@ end erase_lead
 required to be at least as big as the `nat_degree` of the polynomial.  This is useful to prove
 results where you want to change each term in a polynomial to something else depending on the
 `nat_degree` of the polynomial itself and not on the specific `nat_degree` of each term. -/
-lemma induction_with_nat_degree_le {R : Type*} [semiring R] {P : polynomial R → Prop} (N : ℕ)
+lemma induction_with_nat_degree_le (P : polynomial R → Prop) (N : ℕ)
   (P_0 : P 0)
   (P_C_mul_pow : ∀ n : ℕ, ∀ r : R, r ≠ 0 → n ≤ N → P (C r * X ^ n))
-  (P_C_add : ∀ f g : polynomial R, f.nat_degree ≤ N → g.nat_degree ≤ N → P f → P g → P (f + g)) :
+  (P_C_add : ∀ f g : polynomial R, f.nat_degree < g.nat_degree →
+    g.nat_degree ≤ N → P f → P g → P (f + g)) :
   ∀ f : polynomial R, f.nat_degree ≤ N → P f :=
 begin
   intros f df,
@@ -172,18 +173,26 @@ begin
   induction c with c hc,
   { assume f df f0,
     convert P_0,
-    simpa only [support_eq_empty, card_eq_zero] using f0},
-
- --   exact λ f df f0, by rwa (finsupp.support_eq_empty.mp (card_eq_zero.mp f0)) },
+    simpa only [support_eq_empty, card_eq_zero] using f0 },
   { intros f df f0,
-    rw ← erase_lead_add_C_mul_X_pow f,
-    refine P_C_add f.erase_lead _ (erase_lead_nat_degree_le.trans df) _ _ _,
+    rw [← erase_lead_add_C_mul_X_pow f],
+    cases c,
+    { convert P_C_mul_pow f.nat_degree f.leading_coeff _ df,
+      { convert zero_add _,
+        rw [← card_support_eq_zero, erase_lead_card_support f0] },
+      { rw [leading_coeff_ne_zero, ne.def, ← card_support_eq_zero, f0],
+        exact zero_ne_one.symm } },
+    refine P_C_add f.erase_lead _ _ _ _ _,
+    { refine (erase_lead_nat_degree_lt _).trans_le (le_of_eq _),
+      { exact (nat.succ_le_succ (nat.succ_le_succ (nat.zero_le _))).trans f0.ge },
+      { rw [nat_degree_C_mul_X_pow _ _ (leading_coeff_ne_zero.mpr _)],
+        rintro rfl,
+        simpa using f0 } },
     { exact (nat_degree_C_mul_X_pow_le f.leading_coeff f.nat_degree).trans df },
     { exact hc _ (erase_lead_nat_degree_le.trans df) (erase_lead_card_support f0) },
     { refine P_C_mul_pow _ _ _ df,
-      rw [ne.def, leading_coeff_eq_zero],
-      rintro rfl,
-      exact not_le.mpr c.succ_pos f0.ge } }
+      rw [ne.def, leading_coeff_eq_zero, ← card_support_eq_zero, f0],
+      exact nat.succ_ne_zero _ } }
 end
 
 end polynomial