feat(Tactic/ComputeDegree): add helper lemmas for compute_degree_le (…

…#5978)

This PR is a prequel to #5882: it simply adds the helper lemmas about polynomials that the tactic uses.

[Zulip discussion ](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235882.20.60compute_degree_le.60)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib.lean

@@ -2927,6 +2927,7 @@ import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Common
+import Mathlib.Tactic.ComputeDegree
 import Mathlib.Tactic.Congr!
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity

Mathlib/Data/Polynomial/Degree/Definitions.lean

@@ -285,6 +285,8 @@ theorem natDegree_nat_cast (n : ℕ) : natDegree (n : R[X]) = 0 := by
   simp only [← C_eq_nat_cast, natDegree_C]
 #align polynomial.nat_degree_nat_cast Polynomial.natDegree_nat_cast
 
+theorem degree_nat_cast_le (n : ℕ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp)
+
 @[simp]
 theorem degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (monomial n a) = n := by
   rw [degree, support_monomial n ha]; rfl
@@ -537,15 +539,23 @@ theorem coeff_mul_X_sub_C {p : R[X]} {r : R} {a : ℕ} :
 theorem degree_neg (p : R[X]) : degree (-p) = degree p := by unfold degree; rw [support_neg]
 #align polynomial.degree_neg Polynomial.degree_neg
 
+theorem degree_neg_le_of_le {a : WithBot ℕ} {p : R[X]} (hp : degree p ≤ a) : degree (- p) ≤ a :=
+p.degree_neg.le.trans ‹_›
+
 @[simp]
 theorem natDegree_neg (p : R[X]) : natDegree (-p) = natDegree p := by simp [natDegree]
 #align polynomial.nat_degree_neg Polynomial.natDegree_neg
 
+theorem natDegree_neg_le_of_le {p : R[X]} (hp : natDegree p ≤ m) : natDegree (- p) ≤ m :=
+(natDegree_neg p).le.trans ‹_›
+
 @[simp]
 theorem natDegree_int_cast (n : ℤ) : natDegree (n : R[X]) = 0 := by
   rw [← C_eq_int_cast, natDegree_C]
 #align polynomial.nat_degree_int_cast Polynomial.natDegree_int_cast
 
+theorem degree_int_cast_le (n : ℤ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp)
+
 @[simp]
 theorem leadingCoeff_neg (p : R[X]) : (-p).leadingCoeff = -p.leadingCoeff := by
   rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
@@ -643,6 +653,10 @@ theorem degree_add_le_of_degree_le {p q : R[X]} {n : ℕ} (hp : degree p ≤ n)
   (degree_add_le p q).trans <| max_le hp hq
 #align polynomial.degree_add_le_of_degree_le Polynomial.degree_add_le_of_degree_le
 
+theorem degree_add_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) :
+    degree (p + q) ≤ max a b :=
+(p.degree_add_le q).trans <| max_le_max ‹_› ‹_›
+
 theorem natDegree_add_le (p q : R[X]) : natDegree (p + q) ≤ max (natDegree p) (natDegree q) := by
   cases' le_max_iff.1 (degree_add_le p q) with h h <;> simp [natDegree_le_natDegree h]
 #align polynomial.nat_degree_add_le Polynomial.natDegree_add_le
@@ -652,6 +666,10 @@ theorem natDegree_add_le_of_degree_le {p q : R[X]} {n : ℕ} (hp : natDegree p 
   (natDegree_add_le p q).trans <| max_le hp hq
 #align polynomial.nat_degree_add_le_of_degree_le Polynomial.natDegree_add_le_of_degree_le
 
+theorem natDegree_add_le_of_le (hp : natDegree p ≤ m) (hq : natDegree q ≤ n) :
+    natDegree (p + q) ≤ max m n :=
+(p.natDegree_add_le q).trans <| max_le_max ‹_› ‹_›
+
 @[simp]
 theorem leadingCoeff_zero : leadingCoeff (0 : R[X]) = 0 :=
   rfl
@@ -782,6 +800,10 @@ theorem degree_mul_le (p q : R[X]) : degree (p * q) ≤ degree p + degree q :=
       exact add_le_add (le_degree_of_ne_zero ha) (le_degree_of_ne_zero hb)
 #align polynomial.degree_mul_le Polynomial.degree_mul_le
 
+theorem degree_mul_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) :
+    degree (p * q) ≤ a + b :=
+(p.degree_mul_le _).trans <| add_le_add ‹_› ‹_›
+
 theorem degree_pow_le (p : R[X]) : ∀ n : ℕ, degree (p ^ n) ≤ n • degree p
   | 0 => by rw [pow_zero, zero_nsmul]; exact degree_one_le
   | n + 1 =>
@@ -791,6 +813,14 @@ theorem degree_pow_le (p : R[X]) : ∀ n : ℕ, degree (p ^ n) ≤ n • degree
       _ ≤ _ := by rw [succ_nsmul]; exact add_le_add le_rfl (degree_pow_le _ _)
 #align polynomial.degree_pow_le Polynomial.degree_pow_le
 
+theorem degree_pow_le_of_le {a : WithBot ℕ} (b : ℕ) (hp : degree p ≤ a) :
+    degree (p ^ b) ≤ b * a := by
+  induction b with
+  | zero => simp [degree_one_le]
+  | succ n hn =>
+      rw [Nat.cast_succ, add_mul, one_mul, pow_succ']
+      exact degree_mul_le_of_le hn hp
+
 @[simp]
 theorem leadingCoeff_monomial (a : R) (n : ℕ) : leadingCoeff (monomial n a) = a := by
   by_cases ha : a = 0
@@ -1034,6 +1064,10 @@ theorem natDegree_mul_le {p q : R[X]} : natDegree (p * q) ≤ natDegree p + natD
   refine' add_le_add _ _ <;> apply degree_le_natDegree
 #align polynomial.nat_degree_mul_le Polynomial.natDegree_mul_le
 
+theorem natDegree_mul_le_of_le (hp : natDegree p ≤ m) (hg : natDegree q ≤ n) :
+    natDegree (p * q) ≤ m + n :=
+natDegree_mul_le.trans <| add_le_add ‹_› ‹_›
+
 theorem natDegree_pow_le {p : R[X]} {n : ℕ} : (p ^ n).natDegree ≤ n * p.natDegree := by
   induction' n with i hi
   · simp
@@ -1042,6 +1076,10 @@ theorem natDegree_pow_le {p : R[X]} {n : ℕ} : (p ^ n).natDegree ≤ n * p.natD
     exact add_le_add_left hi _
 #align polynomial.nat_degree_pow_le Polynomial.natDegree_pow_le
 
+theorem natDegree_pow_le_of_le (n : ℕ) (hp : natDegree p ≤ m) :
+    natDegree (p ^ n) ≤ n * m :=
+natDegree_pow_le.trans (Nat.mul_le_mul rfl.le ‹_›)
+
 @[simp]
 theorem coeff_pow_mul_natDegree (p : R[X]) (n : ℕ) :
     (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n := by
@@ -1075,6 +1113,8 @@ theorem natDegree_eq_zero_iff_degree_le_zero : p.natDegree = 0 ↔ p.degree ≤
     Nat.cast_withBot, WithBot.coe_zero]
 #align polynomial.nat_degree_eq_zero_iff_degree_le_zero Polynomial.natDegree_eq_zero_iff_degree_le_zero
 
+theorem degree_zero_le : degree (0 : R[X]) ≤ 0 := natDegree_eq_zero_iff_degree_le_zero.mp rfl
+
 theorem degree_le_iff_coeff_zero (f : R[X]) (n : WithBot ℕ) :
     degree f ≤ n ↔ ∀ m : ℕ, n < m → coeff f m = 0 := by
   -- Porting note: `Nat.cast_withBot` is required.
@@ -1294,10 +1334,18 @@ theorem degree_sub_le (p q : R[X]) : degree (p - q) ≤ max (degree p) (degree q
   simpa only [degree_neg q] using degree_add_le p (-q)
 #align polynomial.degree_sub_le Polynomial.degree_sub_le
 
+theorem degree_sub_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) :
+    degree (p - q) ≤ max a b :=
+(p.degree_sub_le q).trans <| max_le_max ‹_› ‹_›
+
 theorem natDegree_sub_le (p q : R[X]) : natDegree (p - q) ≤ max (natDegree p) (natDegree q) := by
   simpa only [← natDegree_neg q] using natDegree_add_le p (-q)
 #align polynomial.nat_degree_sub_le Polynomial.natDegree_sub_le
 
+theorem natDegree_sub_le_of_le (hp : natDegree p ≤ m) (hq : natDegree q ≤ n) :
+    natDegree (p - q) ≤ max m n :=
+(p.natDegree_sub_le q).trans <| max_le_max ‹_› ‹_›
+
 theorem degree_sub_lt (hd : degree p = degree q) (hp0 : p ≠ 0)
     (hlc : leadingCoeff p = leadingCoeff q) : degree (p - q) < degree p :=
   have hp : monomial (natDegree p) (leadingCoeff p) + p.erase (natDegree p) = p :=

Mathlib/Tactic.lean

@@ -24,6 +24,7 @@ import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Common
+import Mathlib.Tactic.ComputeDegree
 import Mathlib.Tactic.Congr!
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity

Mathlib/Tactic/ComputeDegree.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2023 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+
+import Mathlib.Data.Polynomial.Degree.Definitions
+
+/-!
+###  Simple lemmas about `natDegree`
+
+The lemmas in this section all have the form `natDegree <some form of cast> ≤ 0`.
+Their proofs are weakenings of the stronger lemmas `natDegree <same> = 0`.
+These are the lemmas called by `compute_degree_le` on (almost) all the leaves of its recursion.
+-/
+
+open Polynomial
+
+namespace Mathlib.Tactic.ComputeDegree
+
+section leaf_lemmas
+
+variable {R : Type _}
+
+section semiring
+variable [Semiring R]
+
+theorem natDegree_C_le (a : R) : natDegree (C a) ≤ 0 := (natDegree_C a).le
+theorem natDegree_nat_cast_le (n : ℕ) : natDegree (n : R[X]) ≤ 0 := (natDegree_nat_cast _).le
+theorem natDegree_zero_le : natDegree (0 : R[X]) ≤ 0 := natDegree_zero.le
+theorem natDegree_one_le : natDegree (1 : R[X]) ≤ 0 := natDegree_one.le
+
+end semiring
+
+variable [Ring R] in
+theorem natDegree_int_cast_le (n : ℤ) : natDegree (n : R[X]) ≤ 0 := (natDegree_int_cast _).le
+
+end leaf_lemmas
+
+end Mathlib.Tactic.ComputeDegree