refactor(data/polynomial): use monic.ne_zero and nontriviality (#9530)

There is a pattern in `data/polynomial` to have both `(hq : q.monic) (hq0 : q ≠ 0)` as assumptions. I found this less convenient to work with than `[nontrivial R] (hq : q.monic)` and using `monic.ne_zero` to replace `hq0`.

The `nontriviality` tactic automates all the cases where previously `nontrivial R` (or similar) was manually derived from the hypotheses.

Author: Vierkantor

src/data/polynomial/div.lean

@@ -106,14 +106,14 @@ infixl  ` /ₘ ` : 70 := div_by_monic
 
 infixl ` %ₘ ` : 70 := mod_by_monic
 
-lemma degree_mod_by_monic_lt : ∀ (p : polynomial R) {q : polynomial R} (hq : monic q)
-  (hq0 : q ≠ 0), degree (p %ₘ q) < degree q
-| p := λ q hq hq0,
+lemma degree_mod_by_monic_lt [nontrivial R] : ∀ (p : polynomial R) {q : polynomial R}
+  (hq : monic q), degree (p %ₘ q) < degree q
+| p := λ q hq,
 if h : degree q ≤ degree p ∧ p ≠ 0 then
   have wf : _ := div_wf_lemma ⟨h.1, h.2⟩ hq,
   have degree ((p - C (leading_coeff p) * X ^ (nat_degree p - nat_degree q) * q) %ₘ q) < degree q :=
       degree_mod_by_monic_lt (p - C (leading_coeff p) * X ^ (nat_degree p - nat_degree q) * q)
-      hq hq0,
+      hq,
   begin
     unfold mod_by_monic at this ⊢,
     unfold div_mod_by_monic_aux,
@@ -132,7 +132,7 @@ else
     unfold mod_by_monic div_mod_by_monic_aux,
     rw [dif_pos hq, if_neg h, not_not.1 hp],
     exact lt_of_le_of_ne bot_le
-      (ne.symm (mt degree_eq_bot.1 hq0)),
+      (ne.symm (mt degree_eq_bot.1 hq.ne_zero)),
   end
 using_well_founded {dec_tac := tactic.assumption}
 
@@ -164,23 +164,17 @@ lemma div_by_monic_eq_of_not_monic (p : polynomial R) (hq : ¬monic q) : p /ₘ
 
 lemma mod_by_monic_eq_of_not_monic (p : polynomial R) (hq : ¬monic q) : p %ₘ q = p := dif_neg hq
 
-lemma mod_by_monic_eq_self_iff (hq : monic q) (hq0 : q ≠ 0) : p %ₘ q = p ↔ degree p < degree q :=
-⟨λ h, h ▸ degree_mod_by_monic_lt _ hq hq0,
+lemma mod_by_monic_eq_self_iff [nontrivial R] (hq : monic q) : p %ₘ q = p ↔ degree p < degree q :=
+⟨λ h, h ▸ degree_mod_by_monic_lt _ hq,
 λ h, have ¬ degree q ≤ degree p := not_le_of_gt h,
   by unfold mod_by_monic div_mod_by_monic_aux; rw [dif_pos hq, if_neg (mt and.left this)]⟩
 
 theorem degree_mod_by_monic_le (p : polynomial R) {q : polynomial R}
   (hq : monic q) : degree (p %ₘ q) ≤ degree q :=
-decidable.by_cases
-  (assume H : q = 0, by rw [monic, H, leading_coeff_zero] at hq;
-    have : (0:polynomial R) = 1 := (by rw [← C_0, ← C_1, hq]);
-    exact le_of_eq (congr_arg _ $ eq_of_zero_eq_one this (p %ₘ q) q))
-  (assume H : q ≠ 0, le_of_lt $ degree_mod_by_monic_lt _ hq H)
+by { nontriviality R, exact (degree_mod_by_monic_lt _ hq).le }
 
 end ring
 
-
-
 section comm_ring
 variables [comm_ring R] {p q : polynomial R}
 
@@ -209,38 +203,36 @@ using_well_founded {dec_tac := tactic.assumption}
 lemma mod_by_monic_add_div (p : polynomial R) {q : polynomial R} (hq : monic q) :
   p %ₘ q + q * (p /ₘ q) = p := eq_sub_iff_add_eq.1 (mod_by_monic_eq_sub_mul_div p hq)
 
-lemma div_by_monic_eq_zero_iff (hq : monic q) (hq0 : q ≠ 0) : p /ₘ q = 0 ↔ degree p < degree q :=
+lemma div_by_monic_eq_zero_iff [nontrivial R] (hq : monic q) : p /ₘ q = 0 ↔ degree p < degree q :=
 ⟨λ h, by have := mod_by_monic_add_div p hq;
-  rwa [h, mul_zero, add_zero, mod_by_monic_eq_self_iff hq hq0] at this,
+  rwa [h, mul_zero, add_zero, mod_by_monic_eq_self_iff hq] at this,
 λ h, have ¬ degree q ≤ degree p := not_le_of_gt h,
   by unfold div_by_monic div_mod_by_monic_aux; rw [dif_pos hq, if_neg (mt and.left this)]⟩
 
 lemma degree_add_div_by_monic (hq : monic q) (h : degree q ≤ degree p) :
   degree q + degree (p /ₘ q) = degree p :=
-if hq0 : q = 0 then
-  have ∀ (p : polynomial R), p = 0,
-    from λ p, (@subsingleton_of_monic_zero R _ (hq0 ▸ hq)).1 _ _,
-  by rw [this (p /ₘ q), this p, this q]; refl
-else
-have hdiv0 : p /ₘ q ≠ 0 := by rwa [(≠), div_by_monic_eq_zero_iff hq hq0, not_lt],
-have hlc : leading_coeff q * leading_coeff (p /ₘ q) ≠ 0 :=
-  by rwa [monic.def.1 hq, one_mul, (≠), leading_coeff_eq_zero],
-have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
-  calc degree (p %ₘ q) < degree q : degree_mod_by_monic_lt _ hq hq0
-  ... ≤ _ : by rw [degree_mul' hlc, degree_eq_nat_degree hq0,
-      degree_eq_nat_degree hdiv0, ← with_bot.coe_add, with_bot.coe_le_coe];
-    exact nat.le_add_right _ _,
-calc degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) : eq.symm (degree_mul' hlc)
-... = degree (p %ₘ q + q * (p /ₘ q)) : (degree_add_eq_right_of_degree_lt hmod).symm
-... = _ : congr_arg _ (mod_by_monic_add_div _ hq)
+begin
+  nontriviality R,
+  have hdiv0 : p /ₘ q ≠ 0 := by rwa [(≠), div_by_monic_eq_zero_iff hq, not_lt],
+  have hlc : leading_coeff q * leading_coeff (p /ₘ q) ≠ 0 :=
+    by rwa [monic.def.1 hq, one_mul, (≠), leading_coeff_eq_zero],
+  have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
+    calc degree (p %ₘ q) < degree q : degree_mod_by_monic_lt _ hq
+    ... ≤ _ : by rw [degree_mul' hlc, degree_eq_nat_degree hq.ne_zero,
+        degree_eq_nat_degree hdiv0, ← with_bot.coe_add, with_bot.coe_le_coe];
+      exact nat.le_add_right _ _,
+  calc degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) : eq.symm (degree_mul' hlc)
+  ... = degree (p %ₘ q + q * (p /ₘ q)) : (degree_add_eq_right_of_degree_lt hmod).symm
+  ... = _ : congr_arg _ (mod_by_monic_add_div _ hq)
+end
 
 lemma degree_div_by_monic_le (p q : polynomial R) : degree (p /ₘ q) ≤ degree p :=
 if hp0 : p = 0 then by simp only [hp0, zero_div_by_monic, le_refl]
 else if hq : monic q then
-  have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne hp0,
   if h : degree q ≤ degree p
-  then by rw [← degree_add_div_by_monic hq h, degree_eq_nat_degree hq0,
-      degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq hq0).1 (not_lt.2 h))];
+  then by haveI := nontrivial.of_polynomial_ne hp0;
+    rw [← degree_add_div_by_monic hq h, degree_eq_nat_degree hq.ne_zero,
+      degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq).1 (not_lt.2 h))];
     exact with_bot.coe_le_coe.2 (nat.le_add_left _ _)
   else
     by unfold div_by_monic div_mod_by_monic_aux;
@@ -249,17 +241,18 @@ else (div_by_monic_eq_of_not_monic p hq).symm ▸ bot_le
 
 lemma degree_div_by_monic_lt (p : polynomial R) {q : polynomial R} (hq : monic q)
   (hp0 : p ≠ 0) (h0q : 0 < degree q) : degree (p /ₘ q) < degree p :=
-have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne hp0,
 if hpq : degree p < degree q
 then begin
-  rw [(div_by_monic_eq_zero_iff hq hq0).2 hpq, degree_eq_nat_degree hp0],
+  haveI := nontrivial.of_polynomial_ne hp0,
+  rw [(div_by_monic_eq_zero_iff hq).2 hpq, degree_eq_nat_degree hp0],
   exact with_bot.bot_lt_coe _
 end
 else begin
-  rw [← degree_add_div_by_monic hq (not_lt.1 hpq), degree_eq_nat_degree hq0,
-        degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq hq0).1 hpq)],
+  haveI := nontrivial.of_polynomial_ne hp0,
+  rw [← degree_add_div_by_monic hq (not_lt.1 hpq), degree_eq_nat_degree hq.ne_zero,
+        degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq).1 hpq)],
   exact with_bot.coe_lt_coe.2 (nat.lt_add_of_pos_left
-    (with_bot.coe_lt_coe.1 $ (degree_eq_nat_degree hq0) ▸ h0q))
+    (with_bot.coe_lt_coe.1 $ (degree_eq_nat_degree hq.ne_zero) ▸ h0q))
 end
 
 theorem nat_degree_div_by_monic {R : Type u} [comm_ring R] (f : polynomial R) {g : polynomial R}
@@ -271,9 +264,9 @@ begin
         nat_degree_zero] },
   haveI : nontrivial R := ⟨⟨0, 1, h01⟩⟩,
   by_cases hfg : f /ₘ g = 0,
-  { rw [hfg, nat_degree_zero], rw div_by_monic_eq_zero_iff hg hg.ne_zero at hfg,
+  { rw [hfg, nat_degree_zero], rw div_by_monic_eq_zero_iff hg at hfg,
     rw nat.sub_eq_zero_of_le (nat_degree_le_nat_degree $ le_of_lt hfg) },
-  have hgf := hfg, rw div_by_monic_eq_zero_iff hg hg.ne_zero at hgf, push_neg at hgf,
+  have hgf := hfg, rw div_by_monic_eq_zero_iff hg at hgf, push_neg at hgf,
   have := degree_add_div_by_monic hg hgf,
   have hf : f ≠ 0, { intro hf, apply hfg, rw [hf, zero_div_by_monic] },
   rw [degree_eq_nat_degree hf, degree_eq_nat_degree hg.ne_zero, degree_eq_nat_degree hfg,
@@ -283,9 +276,8 @@ end
 
 lemma div_mod_by_monic_unique {f g} (q r : polynomial R) (hg : monic g)
   (h : r + g * q = f ∧ degree r < degree g) : f /ₘ g = q ∧ f %ₘ g = r :=
-if hg0 : g = 0 then by split; exact (subsingleton_of_monic_zero
-  (hg0 ▸ hg : monic (0 : polynomial R))).1 _ _
-else
+begin
+  nontriviality R,
   have h₁ : r - f %ₘ g = -g * (q - f /ₘ g),
     from eq_of_sub_eq_zero
       (by rw [← sub_eq_zero_of_eq (h.1.trans (mod_by_monic_add_div f hg).symm)];
@@ -295,35 +287,34 @@ else
   have h₄ : degree (r - f %ₘ g) < degree g,
     from calc degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) :
       degree_sub_le _ _
-    ... < degree g : max_lt_iff.2 ⟨h.2, degree_mod_by_monic_lt _ hg hg0⟩,
+    ... < degree g : max_lt_iff.2 ⟨h.2, degree_mod_by_monic_lt _ hg⟩,
   have h₅ : q - (f /ₘ g) = 0,
     from by_contradiction
       (λ hqf, not_le_of_gt h₄ $
         calc degree g ≤ degree g + degree (q - f /ₘ g) :
-          by erw [degree_eq_nat_degree hg0, degree_eq_nat_degree hqf,
+          by erw [degree_eq_nat_degree hg.ne_zero, degree_eq_nat_degree hqf,
               with_bot.coe_le_coe];
             exact nat.le_add_right _ _
         ... = degree (r - f %ₘ g) :
           by rw [h₂, degree_mul']; simpa [monic.def.1 hg]),
-  ⟨eq.symm $ eq_of_sub_eq_zero h₅,
+  exact ⟨eq.symm $ eq_of_sub_eq_zero h₅,
     eq.symm $ eq_of_sub_eq_zero $ by simpa [h₅] using h₁⟩
+end
 
 lemma map_mod_div_by_monic [comm_ring S] (f : R →+* S) (hq : monic q) :
   (p /ₘ q).map f = p.map f /ₘ q.map f ∧ (p %ₘ q).map f = p.map f %ₘ q.map f :=
-if h01 : (0 : S) = 1 then by haveI := subsingleton_of_zero_eq_one h01;
-  exact ⟨subsingleton.elim _ _, subsingleton.elim _ _⟩
-else
-have h01R : (0 : R) ≠ 1, from mt (congr_arg f)
-  (by rwa [f.map_one, f.map_zero]),
-have map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q),
-  from (div_mod_by_monic_unique ((p /ₘ q).map f) _ (monic_map f hq)
-    ⟨eq.symm $ by rw [← map_mul, ← map_add, mod_by_monic_add_div _ hq],
-    calc _ ≤ degree (p %ₘ q) : degree_map_le _ _
-    ... < degree q : degree_mod_by_monic_lt _ hq
-      $ (hq.ne_zero_of_ne  h01R)
-    ... = _ : eq.symm $ degree_map_eq_of_leading_coeff_ne_zero _
-      (by rw [monic.def.1 hq, f.map_one]; exact ne.symm h01)⟩),
-⟨this.1.symm, this.2.symm⟩
+begin
+  nontriviality S,
+  haveI : nontrivial R := f.domain_nontrivial,
+  have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q),
+  { exact (div_mod_by_monic_unique ((p /ₘ q).map f) _ (monic_map f hq)
+      ⟨eq.symm $ by rw [← map_mul, ← map_add, mod_by_monic_add_div _ hq],
+      calc _ ≤ degree (p %ₘ q) : degree_map_le _ _
+      ... < degree q : degree_mod_by_monic_lt _ hq
+      ... = _ : eq.symm $ degree_map_eq_of_leading_coeff_ne_zero _
+        (by rw [monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩) },
+  exact ⟨this.1.symm, this.2.symm⟩
+end
 
 lemma map_div_by_monic [comm_ring S] (f : R →+* S) (hq : monic q) :
   (p /ₘ q).map f = p.map f /ₘ q.map f :=
@@ -336,23 +327,23 @@ lemma map_mod_by_monic [comm_ring S] (f : R →+* S) (hq : monic q) :
 lemma dvd_iff_mod_by_monic_eq_zero (hq : monic q) : p %ₘ q = 0 ↔ q ∣ p :=
 ⟨λ h, by rw [← mod_by_monic_add_div p hq, h, zero_add];
   exact dvd_mul_right _ _,
-λ h, if hq0 : q = 0 then by rw hq0 at hq;
-  exact (subsingleton_of_monic_zero hq).1 _ _
-  else
-  let ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h in
-  by_contradiction (λ hpq0,
-  have hmod : p %ₘ q = q * (r - p /ₘ q) :=
-    by rw [mod_by_monic_eq_sub_mul_div _ hq, mul_sub, ← hr],
-  have degree (q * (r - p /ₘ q)) < degree q :=
-    hmod ▸ degree_mod_by_monic_lt _ hq hq0,
+λ h, begin
+  nontriviality R,
+  obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h,
+  by_contradiction hpq0,
+  have hmod : p %ₘ q = q * (r - p /ₘ q),
+  { rw [mod_by_monic_eq_sub_mul_div _ hq, mul_sub, ← hr] },
+  have : degree (q * (r - p /ₘ q)) < degree q :=
+    hmod ▸ degree_mod_by_monic_lt _ hq,
   have hrpq0 : leading_coeff (r - p /ₘ q) ≠ 0 :=
     λ h, hpq0 $ leading_coeff_eq_zero.1
       (by rw [hmod, leading_coeff_eq_zero.1 h, mul_zero, leading_coeff_zero]),
   have hlc : leading_coeff q * leading_coeff (r - p /ₘ q) ≠ 0 :=
     by rwa [monic.def.1 hq, one_mul],
-  by rw [degree_mul' hlc, degree_eq_nat_degree hq0,
-      degree_eq_nat_degree (mt leading_coeff_eq_zero.2 hrpq0)] at this;
-    exact not_lt_of_ge (nat.le_add_right _ _) (with_bot.some_lt_some.1 this))⟩
+  rw [degree_mul' hlc, degree_eq_nat_degree hq.ne_zero,
+      degree_eq_nat_degree (mt leading_coeff_eq_zero.2 hrpq0)] at this,
+    exact not_lt_of_ge (nat.le_add_right _ _) (with_bot.some_lt_some.1 this)
+end⟩
 
 theorem map_dvd_map [comm_ring S] (f : R →+* S) (hf : function.injective f) {x y : polynomial R}
   (hx : x.monic) : x.map f ∣ y.map f ↔ x ∣ y :=
@@ -371,22 +362,17 @@ by conv_rhs { rw [← mod_by_monic_add_div p monic_one] }; simp
 
 @[simp] lemma mod_by_monic_X_sub_C_eq_C_eval (p : polynomial R) (a : R) :
   p %ₘ (X - C a) = C (p.eval a) :=
-if h0 : (0 : R) = 1 then by letI := subsingleton_of_zero_eq_one h0; exact subsingleton.elim _ _
-else
-by haveI : nontrivial R := nontrivial_of_ne 0 1 h0; exact
-have h : (p %ₘ (X - C a)).eval a = p.eval a :=
-  by rw [mod_by_monic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul,
-    eval_sub, eval_X, eval_C, sub_self, zero_mul, sub_zero],
-have degree (p %ₘ (X - C a)) < 1 :=
-  degree_X_sub_C a ▸ degree_mod_by_monic_lt p (monic_X_sub_C a) ((degree_X_sub_C a).symm ▸
-    ne_zero_of_monic (monic_X_sub_C _)),
-have degree (p %ₘ (X - C a)) ≤ 0 :=
-  begin
-    cases (degree (p %ₘ (X - C a))),
-    { exact bot_le },
-    { exact with_bot.some_le_some.2 (nat.le_of_lt_succ (with_bot.some_lt_some.1 this)) }
-  end,
 begin
+  nontriviality R,
+  have h : (p %ₘ (X - C a)).eval a = p.eval a,
+  { rw [mod_by_monic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul,
+        eval_sub, eval_X, eval_C, sub_self, zero_mul, sub_zero] },
+  have : degree (p %ₘ (X - C a)) < 1 :=
+    degree_X_sub_C a ▸ degree_mod_by_monic_lt p (monic_X_sub_C a),
+  have : degree (p %ₘ (X - C a)) ≤ 0,
+  { cases (degree (p %ₘ (X - C a))),
+    { exact bot_le },
+    { exact with_bot.some_le_some.2 (nat.le_of_lt_succ (with_bot.some_lt_some.1 this)) } },
   rw [eq_C_of_degree_le_zero this, eval_C] at h,
   rw [eq_C_of_degree_le_zero this, h]
 end

src/data/polynomial/field_division.lean

@@ -121,8 +121,6 @@ private lemma remainder_lt_aux (p : polynomial R) (hq : q ≠ 0) :
   degree (mod p q) < degree q :=
 by rw ← degree_mul_leading_coeff_inv q hq; exact
   degree_mod_by_monic_lt p (monic_mul_leading_coeff_inv hq)
-    (mul_ne_zero hq (mt leading_coeff_eq_zero.2 (by rw leading_coeff_C;
-      exact inv_ne_zero (mt leading_coeff_eq_zero.1 hq))))
 
 instance : has_div (polynomial R) := ⟨div⟩
 
@@ -173,7 +171,7 @@ lemma div_eq_zero_iff (hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q :=
 λ h, have hlt : degree p < degree (q * C (leading_coeff q)⁻¹),
     by rwa degree_mul_leading_coeff_inv q hq0,
   have hm : monic (q * C (leading_coeff q)⁻¹) := monic_mul_leading_coeff_inv hq0,
-  by rw [div_def, (div_by_monic_eq_zero_iff hm (ne_zero_of_monic hm)).2 hlt, mul_zero]⟩
+  by rw [div_def, (div_by_monic_eq_zero_iff hm).2 hlt, mul_zero]⟩
 
 lemma degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) :
   degree q + degree (p / q) = degree p :=

src/data/polynomial/ring_division.lean

@@ -253,8 +253,8 @@ then
     rw degree_eq_nat_degree hp at hpd,
     exact with_bot.coe_le_coe.2 (with_bot.coe_lt_coe.1 hpd)
   end,
-  have hdiv0 : p /ₘ (X - C x) ≠ 0 := mt (div_by_monic_eq_zero_iff (monic_X_sub_C x)
-    (ne_zero_of_monic (monic_X_sub_C x))).1 $ not_lt.2 hdeg,
+  have hdiv0 : p /ₘ (X - C x) ≠ 0 := mt (div_by_monic_eq_zero_iff (monic_X_sub_C x)).1 $
+    not_lt.2 hdeg,
   ⟨x ::ₘ t, calc (card (x ::ₘ t) : with_bot ℕ) = t.card + 1 :
       by exact_mod_cast card_cons _ _
     ... ≤ degree p :
@@ -577,10 +577,10 @@ begin
   have hp := mod_by_monic_add_div p hmonic,
   have hzero : (p /ₘ q) ≠ 0,
   { intro h,
-    exact not_lt_of_le hdegree ((div_by_monic_eq_zero_iff hmonic (monic.ne_zero hmonic)).1 h) },
+    exact not_lt_of_le hdegree ((div_by_monic_eq_zero_iff hmonic).1 h) },
   have deglt : (p %ₘ q).degree < (q * (p /ₘ q)).degree,
   { rw degree_mul,
-    refine lt_of_lt_of_le (degree_mod_by_monic_lt p hmonic (monic.ne_zero hmonic)) _,
+    refine lt_of_lt_of_le (degree_mod_by_monic_lt p hmonic) _,
     rw [degree_eq_nat_degree (monic.ne_zero hmonic), degree_eq_nat_degree hzero],
     norm_cast,
     simp only [zero_le, le_add_iff_nonneg_right] },

src/field_theory/minpoly.lean

@@ -289,7 +289,7 @@ begin
   by_contra hnz,
   have := degree_le_of_ne_zero A x hnz _,
   { contrapose! this,
-    exact degree_mod_by_monic_lt _ (monic hx) (ne_zero hx) },
+    exact degree_mod_by_monic_lt _ (monic hx) },
   { rw ← mod_by_monic_add_div p (monic hx) at hp,
     simpa using hp }
 end

src/ring_theory/power_basis.lean

@@ -251,8 +251,7 @@ begin
   have : (f %ₘ minpoly A pb.gen).nat_degree < pb.dim,
   { rw ← pb.nat_degree_minpoly,
     apply nat_degree_lt_nat_degree hf,
-    exact degree_mod_by_monic_lt _ (minpoly.monic pb.is_integral_gen)
-      (minpoly.ne_zero pb.is_integral_gen) },
+    exact degree_mod_by_monic_lt _ (minpoly.monic pb.is_integral_gen) },
   rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, linear_map.map_sum],
   refine finset.sum_congr rfl (λ i (hi : i ∈ finset.range pb.dim), _),
   rw finset.mem_range at hi,
@@ -435,7 +434,7 @@ begin
   apply mem_span_pow'.mpr _,
   have := minpoly.monic hx,
   refine ⟨f.mod_by_monic (minpoly R x),
-      lt_of_lt_of_le (degree_mod_by_monic_lt _ this (ne_zero_of_monic this)) degree_le_nat_degree,
+      lt_of_lt_of_le (degree_mod_by_monic_lt _ this) degree_le_nat_degree,
       _⟩,
   conv_lhs { rw ← mod_by_monic_add_div f this },
   simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, alg_hom.map_mul]