From ac976755c62166345eb53dd5c785146144128973 Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Thu, 30 Dec 2021 14:54:46 +0000
Subject: [PATCH] feat(data/polynomial/degree/definition): nat_degree_monomial
 in ite form (#11123)

Changed the proof usage elsewhere.
This helps deal with sums of over monomials.
---
 src/data/polynomial/degree/definitions.lean | 12 ++++++++----
 src/data/polynomial/erase_lead.lean         |  2 +-
 src/data/polynomial/mirror.lean             |  3 ++-
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean
index 4a3735ced394a..027cba85836ff 100644
--- a/src/data/polynomial/degree/definitions.lean
+++ b/src/data/polynomial/degree/definitions.lean
@@ -198,9 +198,13 @@ nat_degree_eq_of_degree_eq_some (degree_C_mul_X_pow n ha)
 @[simp] lemma nat_degree_C_mul_X (a : R) (ha : a ≠ 0) : nat_degree (C a * X) = 1 :=
 by simpa only [pow_one] using nat_degree_C_mul_X_pow 1 a ha
 
-@[simp] lemma nat_degree_monomial (i : ℕ) (r : R) (hr : r ≠ 0) :
-  nat_degree (monomial i r) = i :=
-by rw [← C_mul_X_pow_eq_monomial, nat_degree_C_mul_X_pow i r hr]
+@[simp] lemma nat_degree_monomial [decidable_eq R] (i : ℕ) (r : R)  :
+  nat_degree (monomial i r) = if r = 0 then 0 else i :=
+begin
+  split_ifs with hr,
+  { simp [hr] },
+  { rw [← C_mul_X_pow_eq_monomial, nat_degree_C_mul_X_pow i r hr] }
+end
 
 lemma coeff_eq_zero_of_degree_lt (h : degree p < n) : coeff p n = 0 :=
 not_not.1 (mt le_degree_of_ne_zero (not_le_of_gt h))
@@ -561,7 +565,7 @@ lemma degree_pow_le (p : polynomial R) : ∀ (n : ℕ), degree (p ^ n) ≤ n •
 begin
   by_cases ha : a = 0,
   { simp only [ha, (monomial n).map_zero, leading_coeff_zero] },
-  { rw [leading_coeff, nat_degree_monomial _ _ ha, coeff_monomial], simp }
+  { rw [leading_coeff, nat_degree_monomial, if_neg ha, coeff_monomial], simp }
 end
 
 lemma leading_coeff_C_mul_X_pow (a : R) (n : ℕ) : leading_coeff (C a * X ^ n) = a :=
diff --git a/src/data/polynomial/erase_lead.lean b/src/data/polynomial/erase_lead.lean
index 26bdf624fcccf..28010635ef52b 100644
--- a/src/data/polynomial/erase_lead.lean
+++ b/src/data/polynomial/erase_lead.lean
@@ -111,7 +111,7 @@ erase_lead_card_support fc
 begin
   by_cases hr : r = 0,
   { subst r, simp only [monomial_zero_right, erase_lead_zero] },
-  { rw [erase_lead, nat_degree_monomial _ _ hr, erase_monomial] }
+  { rw [erase_lead, nat_degree_monomial, if_neg hr, erase_monomial] }
 end
 
 @[simp] lemma erase_lead_C (r : R) : erase_lead (C r) = 0 :=
diff --git a/src/data/polynomial/mirror.lean b/src/data/polynomial/mirror.lean
index 5564f7f5247fd..a2cf132a655d2 100644
--- a/src/data/polynomial/mirror.lean
+++ b/src/data/polynomial/mirror.lean
@@ -40,9 +40,10 @@ noncomputable def mirror := p.reverse * X ^ p.nat_trailing_degree
 
 lemma mirror_monomial (n : ℕ) (a : R) : (monomial n a).mirror = (monomial n a) :=
 begin
+  classical,
   by_cases ha : a = 0,
   { rw [ha, monomial_zero_right, mirror_zero] },
-  { rw [mirror, reverse, nat_degree_monomial n a ha, nat_trailing_degree_monomial ha,
+  { rw [mirror, reverse, nat_degree_monomial n a, if_neg ha, nat_trailing_degree_monomial ha,
         ←C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, rev_at_le (le_refl n),
         tsub_self, pow_zero, mul_one] },
 end