diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean
index ee1bf0b8fab00..90d4ee6e88f83 100644
--- a/src/data/polynomial/degree/definitions.lean
+++ b/src/data/polynomial/degree/definitions.lean
@@ -656,6 +656,18 @@ begin
   refl
 end
 
+lemma monomial_nat_degree_leading_coeff_eq_self (h : p.support.card ≤ 1) :
+  monomial p.nat_degree p.leading_coeff = p :=
+begin
+  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩,
+  by_cases ha : a = 0;
+  simp [ha]
+end
+
+lemma C_mul_X_pow_eq_self (h : p.support.card ≤ 1) :
+  C p.leading_coeff * X^p.nat_degree = p :=
+by rw [C_mul_X_pow_eq_monomial, monomial_nat_degree_leading_coeff_eq_self h]
+
 lemma leading_coeff_pow' : leading_coeff p ^ n ≠ 0 →
   leading_coeff (p ^ n) = leading_coeff p ^ n :=
 nat.rec_on n (by simp) $
diff --git a/src/data/polynomial/degree/lemmas.lean b/src/data/polynomial/degree/lemmas.lean
index ff2759e8da78d..3f96e3a041248 100644
--- a/src/data/polynomial/degree/lemmas.lean
+++ b/src/data/polynomial/degree/lemmas.lean
@@ -49,27 +49,6 @@ else with_bot.coe_le_coe.1 $
         (le_nat_degree_of_ne_zero (mem_support_iff.1 hn))
         (nat.zero_le _))
 
-lemma degree_map_eq_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
-  (hf : f (leading_coeff p) ≠ 0) : degree (p.map f) = degree p :=
-le_antisymm (degree_map_le f _) $
-  have hp0 : p ≠ 0, from λ hp0, by simpa [hp0, f.map_zero] using hf,
-  begin
-    rw [degree_eq_nat_degree hp0],
-    refine le_degree_of_ne_zero _,
-    rw [coeff_map], exact hf
-  end
-
-lemma nat_degree_map_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
-  (hf : f (leading_coeff p) ≠ 0) : nat_degree (p.map f) = nat_degree p :=
-nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f hf)
-
-lemma leading_coeff_map_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
-  (hf : f (leading_coeff p) ≠ 0) : leading_coeff (p.map f) = f (leading_coeff p) :=
-begin
-  unfold leading_coeff,
-  rw [coeff_map, nat_degree_map_of_leading_coeff_ne_zero f hf],
-end
-
 lemma degree_pos_of_root {p : polynomial R} (hp : p ≠ 0) (h : is_root p a) : 0 < degree p :=
 lt_of_not_ge $ λ hlt, begin
   have := eq_C_of_degree_le_zero hlt,
@@ -165,59 +144,6 @@ lemma degree_pos_of_eval₂_root {p : polynomial R} (hp : p ≠ 0) (f : R →+*
   0 < degree p :=
 nat_degree_pos_iff_degree_pos.mp (nat_degree_pos_of_eval₂_root hp f hz inj)
 
-section injective
-open function
-variables {f : R →+* S} (hf : injective f)
-include hf
-
-lemma degree_map_eq_of_injective (p : polynomial R) : degree (p.map f) = degree p :=
-if h : p = 0 then by simp [h]
-else degree_map_eq_of_leading_coeff_ne_zero _
-  (by rw [← f.map_zero]; exact mt hf.eq_iff.1
-    (mt leading_coeff_eq_zero.1 h))
-
-lemma degree_map' (p : polynomial R) :
-  degree (p.map f) = degree p :=
-p.degree_map_eq_of_injective hf
-
-lemma nat_degree_map' (p : polynomial R) :
-  nat_degree (p.map f) = nat_degree p :=
-nat_degree_eq_of_degree_eq (degree_map' hf p)
-
-lemma leading_coeff_map' (p : polynomial R) :
-  leading_coeff (p.map f) = f (leading_coeff p) :=
-begin
-  unfold leading_coeff,
-  rw [coeff_map, nat_degree_map' hf p],
-end
-
-lemma next_coeff_map (p : polynomial R) :
-  (p.map f).next_coeff = f p.next_coeff :=
-begin
-  unfold next_coeff,
-  rw nat_degree_map' hf,
-  split_ifs; simp
-end
-
-end injective
-
-section
-variable {f : polynomial R}
-
-lemma monomial_nat_degree_leading_coeff_eq_self (h : f.support.card ≤ 1) :
-  monomial f.nat_degree f.leading_coeff = f :=
-begin
-  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩,
-  by_cases ha : a = 0;
-  simp [ha]
-end
-
-lemma C_mul_X_pow_eq_self (h : f.support.card ≤ 1) :
-  C f.leading_coeff * X^f.nat_degree = f :=
-by rw [C_mul_X_pow_eq_monomial, monomial_nat_degree_leading_coeff_eq_self h]
-
-end
-
 end degree
 end semiring
 
diff --git a/src/data/polynomial/denoms_clearable.lean b/src/data/polynomial/denoms_clearable.lean
index fe03f8eea413b..36cde53bb0090 100644
--- a/src/data/polynomial/denoms_clearable.lean
+++ b/src/data/polynomial/denoms_clearable.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import data.polynomial.erase_lead
+import data.polynomial.eval
+
 /-!
 # Denominators of evaluation of polynomials at ratios
 
diff --git a/src/data/polynomial/div.lean b/src/data/polynomial/div.lean
index 39ef3af90ed4f..279fbe160deaf 100644
--- a/src/data/polynomial/div.lean
+++ b/src/data/polynomial/div.lean
@@ -19,113 +19,10 @@ noncomputable theory
 open_locale classical big_operators
 
 open finset
-
 namespace polynomial
 universes u v w z
 variables {R : Type u} {S : Type v} {T : Type w} {A : Type z} {a b : R} {n : ℕ}
 
-section semiring
-variables [semiring R] {p q : polynomial R}
-
-/-- `div_X p` return a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
-  It can be used in a semiring where the usual division algorithm is not possible -/
-def div_X (p : polynomial R) : polynomial R :=
-∑ n in Ico 0 p.nat_degree, monomial n (p.coeff (n + 1))
-
-@[simp] lemma coeff_div_X : (div_X p).coeff n = p.coeff (n+1) :=
-begin
-  simp only [div_X, coeff_monomial, true_and, finset_sum_coeff, not_lt,
-    Ico.mem, zero_le, finset.sum_ite_eq', ite_eq_left_iff],
-  intro h,
-  rw coeff_eq_zero_of_nat_degree_lt (nat.lt_succ_of_le h)
-end
-
-lemma div_X_mul_X_add (p : polynomial R) : div_X p * X + C (p.coeff 0) = p :=
-ext $ by rintro ⟨_|_⟩; simp [coeff_C, nat.succ_ne_zero, coeff_mul_X]
-
-@[simp] lemma div_X_C (a : R) : div_X (C a) = 0 :=
-ext $ λ n, by cases n; simp [div_X, coeff_C]; simp [coeff]
-
-lemma div_X_eq_zero_iff : div_X p = 0 ↔ p = C (p.coeff 0) :=
-⟨λ h, by simpa [eq_comm, h] using div_X_mul_X_add p,
-  λ h, by rw [h, div_X_C]⟩
-
-lemma div_X_add : div_X (p + q) = div_X p + div_X q :=
-ext $ by simp
-
-lemma degree_div_X_lt (hp0 : p ≠ 0) : (div_X p).degree < p.degree :=
-by haveI := nontrivial.of_polynomial_ne hp0;
-calc (div_X p).degree < (div_X p * X + C (p.coeff 0)).degree :
-  if h : degree p ≤ 0
-  then begin
-      have h' : C (p.coeff 0) ≠ 0, by rwa [← eq_C_of_degree_le_zero h],
-      rw [eq_C_of_degree_le_zero h, div_X_C, degree_zero, zero_mul, zero_add],
-      exact lt_of_le_of_ne bot_le (ne.symm (mt degree_eq_bot.1 $
-        by simp [h'])),
-    end
-  else
-    have hXp0 : div_X p ≠ 0,
-      by simpa [div_X_eq_zero_iff, -not_le, degree_le_zero_iff] using h,
-    have leading_coeff (div_X p) * leading_coeff X ≠ 0, by simpa,
-    have degree (C (p.coeff 0)) < degree (div_X p * X),
-      from calc degree (C (p.coeff 0)) ≤ 0 : degree_C_le
-         ... < 1 : dec_trivial
-         ... = degree (X : polynomial R) : degree_X.symm
-         ... ≤ degree (div_X p * X) :
-          by rw [← zero_add (degree X), degree_mul' this];
-            exact add_le_add
-              (by rw [zero_le_degree_iff, ne.def, div_X_eq_zero_iff];
-                exact λ h0, h (h0.symm ▸ degree_C_le))
-              (le_refl _),
-    by rw [degree_add_eq_left_of_degree_lt this];
-      exact degree_lt_degree_mul_X hXp0
-... = p.degree : by rw div_X_mul_X_add
-
-/-- An induction principle for polynomials, valued in Sort* instead of Prop. -/
-@[elab_as_eliminator] noncomputable def rec_on_horner
-  {M : polynomial R → Sort*} : Π (p : polynomial R),
-  M 0 →
-  (Π p a, coeff p 0 = 0 → a ≠ 0 → M p → M (p + C a)) →
-  (Π p, p ≠ 0 → M p → M (p * X)) →
-  M p
-| p := λ M0 MC MX,
-if hp : p = 0 then eq.rec_on hp.symm M0
-else
-have wf : degree (div_X p) < degree p,
-  from degree_div_X_lt hp,
-by rw [← div_X_mul_X_add p] at *;
-  exact
-  if hcp0 : coeff p 0 = 0
-  then by rw [hcp0, C_0, add_zero];
-    exact MX _ (λ h : div_X p = 0, by simpa [h, hcp0] using hp)
-      (rec_on_horner _ M0 MC MX)
-  else MC _ _ (coeff_mul_X_zero _) hcp0 (if hpX0 : div_X p = 0
-    then show M (div_X p * X), by rw [hpX0, zero_mul]; exact M0
-    else MX (div_X p) hpX0 (rec_on_horner _ M0 MC MX))
-using_well_founded {dec_tac := tactic.assumption}
-
-@[elab_as_eliminator] lemma degree_pos_induction_on
-  {P : polynomial R → Prop} (p : polynomial R) (h0 : 0 < degree p)
-  (hC : ∀ {a}, a ≠ 0 → P (C a * X))
-  (hX : ∀ {p}, 0 < degree p → P p → P (p * X))
-  (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
-rec_on_horner p
-  (λ h, by rw degree_zero at h; exact absurd h dec_trivial)
-  (λ p a _ _ ih h0,
-    have 0 < degree p,
-      from lt_of_not_ge (λ h, (not_lt_of_ge degree_C_le) $
-        by rwa [eq_C_of_degree_le_zero h, ← C_add] at h0),
-    hadd this (ih this))
-  (λ p _ ih h0',
-    if h0 : 0 < degree p
-    then hX h0 (ih h0)
-    else by rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at *;
-      exact hC (λ h : coeff p 0 = 0,
-        by simpa [h, nat.not_lt_zero] using h0'))
-  h0
-
-end semiring
-
 section comm_semiring
 variables [comm_semiring R]
 
diff --git a/src/data/polynomial/erase_lead.lean b/src/data/polynomial/erase_lead.lean
index c17b0e7673ad4..3456ab2949a85 100644
--- a/src/data/polynomial/erase_lead.lean
+++ b/src/data/polynomial/erase_lead.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import data.polynomial.degree
 import data.polynomial.degree.trailing_degree
+import data.polynomial.inductions
 
 /-!
 # Erase the leading term of a univariate polynomial
diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
index 66ed647c6893b..b4013c6a8b488 100644
--- a/src/data/polynomial/eval.lean
+++ b/src/data/polynomial/eval.lean
@@ -389,8 +389,8 @@ eval₂_monomial _ _
 @[simp] lemma mul_X_comp : (p * X).comp r = p.comp r * r :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq, add_mul], },
-  { intros n b, simp [pow_succ', mul_assoc], }
+  { intros p q hp hq, simp only [hp, hq, add_mul, add_comp] },
+  { intros n b, simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp] }
 end
 
 @[simp] lemma X_pow_comp {k : ℕ} : (X^k).comp p = p^k :=
@@ -529,14 +529,35 @@ nat_degree_le_nat_degree (degree_map_le f p)
 variables {f}
 
 lemma map_monic_eq_zero_iff (hp : p.monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
-⟨ λ hfp x, calc f x = f x * f p.leading_coeff : by simp [hp]
-                ... = f x * (p.map f).coeff p.nat_degree : by { congr, apply (coeff_map _ _).symm }
-                ... = 0 : by simp [hfp],
-  λ h, ext (λ n, by simp [h]) ⟩
+⟨ λ hfp x, calc f x = f x * f p.leading_coeff : by simp only [mul_one, hp.leading_coeff, f.map_one]
+                ... = f x * (p.map f).coeff p.nat_degree : congr_arg _ (coeff_map _ _).symm
+                ... = 0 : by simp only [hfp, mul_zero, coeff_zero],
+  λ h, ext (λ n, by simp only [h, coeff_map, coeff_zero]) ⟩
 
 lemma map_monic_ne_zero (hp : p.monic) [nontrivial S] : p.map f ≠ 0 :=
 λ h, f.map_one_ne_zero ((map_monic_eq_zero_iff hp).mp h _)
 
+lemma degree_map_eq_of_leading_coeff_ne_zero (f : R →+* S)
+  (hf : f (leading_coeff p) ≠ 0) : degree (p.map f) = degree p :=
+le_antisymm (degree_map_le f _) $
+  have hp0 : p ≠ 0, from leading_coeff_ne_zero.mp (λ hp0, hf (trans (congr_arg _ hp0) f.map_zero)),
+  begin
+    rw [degree_eq_nat_degree hp0],
+    refine le_degree_of_ne_zero _,
+    rw [coeff_map], exact hf
+  end
+
+lemma nat_degree_map_of_leading_coeff_ne_zero (f : R →+* S)
+  (hf : f (leading_coeff p) ≠ 0) : nat_degree (p.map f) = nat_degree p :=
+nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f hf)
+
+lemma leading_coeff_map_of_leading_coeff_ne_zero (f : R →+* S)
+  (hf : f (leading_coeff p) ≠ 0) : leading_coeff (p.map f) = f (leading_coeff p) :=
+begin
+  unfold leading_coeff,
+  rw [coeff_map, nat_degree_map_of_leading_coeff_ne_zero f hf],
+end
+
 variables (f)
 
 @[simp] lemma map_ring_hom_id : map_ring_hom (ring_hom.id R) = ring_hom.id (polynomial R) :=
@@ -575,8 +596,9 @@ begin
     (nat_degree_map_le _ _).trans_lt (nat.lt_succ_self _),
   conv_lhs { rw [eval₂_eq_sum], },
   rw [sum_over_range' _ _ _ A],
-  { simp [coeff_map, eval₂_eq_sum, sum_over_range] },
-  { simp }
+  { simp only [coeff_map, eval₂_eq_sum, sum_over_range, forall_const, zero_mul, ring_hom.map_zero,
+      function.comp_app, ring_hom.coe_comp] },
+  { simp only [forall_const, zero_mul, ring_hom.map_zero] }
 end
 
 lemma eval_map (x : S) : (p.map f).eval x = p.eval₂ f x :=
@@ -588,9 +610,11 @@ lemma map_sum {ι : Type*} (g : ι → polynomial R) (s : finset ι) :
 
 lemma map_comp (p q : polynomial R) : map f (p.comp q) = (map f p).comp (map f q) :=
 polynomial.induction_on p
-  (by simp)
-  (by simp {contextual := tt})
-  (by simp [pow_succ', ← mul_assoc, polynomial.comp] {contextual := tt})
+  (by simp only [map_C, forall_const, C_comp, eq_self_iff_true])
+  (by simp only [map_add, add_comp, forall_const, implies_true_iff, eq_self_iff_true]
+        {contextual := tt})
+  (by simp only [pow_succ', ←mul_assoc, comp, forall_const, eval₂_mul_X, implies_true_iff,
+        eq_self_iff_true, map_X, map_mul] {contextual := tt})
 
 @[simp]
 lemma eval_zero_map (f : R →+* S) (p : polynomial R) :
@@ -602,8 +626,8 @@ lemma eval_one_map (f : R →+* S) (p : polynomial R) :
   (p.map f).eval 1 = f (p.eval 1) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq], },
-  { intros n r, simp, }
+  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros n r, simp only [one_pow, mul_one, eval_monomial, map_monomial] }
 end
 
 @[simp]
@@ -611,8 +635,8 @@ lemma eval_nat_cast_map (f : R →+* S) (p : polynomial R) (n : ℕ) :
   (p.map f).eval n = f (p.eval n) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq], },
-  { intros n r, simp, }
+  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros n r, simp only [f.map_nat_cast, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
 end
 
 @[simp]
@@ -621,8 +645,8 @@ lemma eval_int_cast_map {R S : Type*} [ring R] [ring S]
   (p.map f).eval i = f (p.eval i) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq], },
-  { intros n r, simp, }
+  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros n r, simp only [f.map_int_cast, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
 end
 
 end map
@@ -643,11 +667,9 @@ variables (f : R →+* S) (g : S →+* T) (p)
 lemma hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) :=
 begin
   apply polynomial.induction_on p; clear p,
-  { intros a, rw [eval₂_C, eval₂_C], refl, },
+  { simp only [forall_const, eq_self_iff_true, eval₂_C, ring_hom.coe_comp] },
   { intros p q hp hq, simp only [hp, hq, eval₂_add, g.map_add] },
-  { intros n a ih,
-    simp only [eval₂_mul, eval₂_C, eval₂_X_pow, g.map_mul, g.map_pow],
-    refl, }
+  { intros n a ih, simpa only [eval₂_mul, eval₂_C, eval₂_X_pow, g.map_mul, g.map_pow] }
 end
 
 end hom_eval₂
@@ -731,7 +753,6 @@ begin
   intros x,
   simp only [mem_support_iff],
   contrapose!,
-  change p.coeff x = 0 → (map f p).coeff x = 0,
   rw coeff_map,
   intro hx,
   rw hx,
diff --git a/src/data/polynomial/inductions.lean b/src/data/polynomial/inductions.lean
new file mode 100644
index 0000000000000..ddd36e8e67022
--- /dev/null
+++ b/src/data/polynomial/inductions.lean
@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2021 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Damiano Testa, Jens Wagemaker
+-/
+import data.polynomial.degree.definitions
+import data.finset.intervals
+
+/-!
+# Induction on polynomials
+
+This file contains lemmas dealing with different flavours of induction on polynomials.
+-/
+
+noncomputable theory
+open_locale classical big_operators
+
+open finset
+
+namespace polynomial
+universes u v w z
+variables {R : Type u} {S : Type v} {T : Type w} {A : Type z} {a b : R} {n : ℕ}
+
+section semiring
+variables [semiring R] {p q : polynomial R}
+
+/-- `div_X p` returns a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
+  It can be used in a semiring where the usual division algorithm is not possible -/
+def div_X (p : polynomial R) : polynomial R :=
+∑ n in Ico 0 p.nat_degree, monomial n (p.coeff (n + 1))
+
+@[simp] lemma coeff_div_X : (div_X p).coeff n = p.coeff (n+1) :=
+begin
+  simp only [div_X, coeff_monomial, true_and, finset_sum_coeff, not_lt,
+    Ico.mem, zero_le, finset.sum_ite_eq', ite_eq_left_iff],
+  intro h,
+  rw coeff_eq_zero_of_nat_degree_lt (nat.lt_succ_of_le h)
+end
+
+lemma div_X_mul_X_add (p : polynomial R) : div_X p * X + C (p.coeff 0) = p :=
+ext $ by rintro ⟨_|_⟩; simp [coeff_C, nat.succ_ne_zero, coeff_mul_X]
+
+@[simp] lemma div_X_C (a : R) : div_X (C a) = 0 :=
+ext $ λ n, by cases n; simp [div_X, coeff_C]; simp [coeff]
+
+lemma div_X_eq_zero_iff : div_X p = 0 ↔ p = C (p.coeff 0) :=
+⟨λ h, by simpa [eq_comm, h] using div_X_mul_X_add p,
+  λ h, by rw [h, div_X_C]⟩
+
+lemma div_X_add : div_X (p + q) = div_X p + div_X q :=
+ext $ by simp
+
+lemma degree_div_X_lt (hp0 : p ≠ 0) : (div_X p).degree < p.degree :=
+by haveI := nontrivial.of_polynomial_ne hp0;
+calc (div_X p).degree < (div_X p * X + C (p.coeff 0)).degree :
+  if h : degree p ≤ 0
+  then begin
+      have h' : C (p.coeff 0) ≠ 0, by rwa [← eq_C_of_degree_le_zero h],
+      rw [eq_C_of_degree_le_zero h, div_X_C, degree_zero, zero_mul, zero_add],
+      exact lt_of_le_of_ne bot_le (ne.symm (mt degree_eq_bot.1 $
+        by simp [h'])),
+    end
+  else
+    have hXp0 : div_X p ≠ 0,
+      by simpa [div_X_eq_zero_iff, -not_le, degree_le_zero_iff] using h,
+    have leading_coeff (div_X p) * leading_coeff X ≠ 0, by simpa,
+    have degree (C (p.coeff 0)) < degree (div_X p * X),
+      from calc degree (C (p.coeff 0)) ≤ 0 : degree_C_le
+         ... < 1 : dec_trivial
+         ... = degree (X : polynomial R) : degree_X.symm
+         ... ≤ degree (div_X p * X) :
+          by rw [← zero_add (degree X), degree_mul' this];
+            exact add_le_add
+              (by rw [zero_le_degree_iff, ne.def, div_X_eq_zero_iff];
+                exact λ h0, h (h0.symm ▸ degree_C_le))
+              (le_refl _),
+    by rw [degree_add_eq_left_of_degree_lt this];
+      exact degree_lt_degree_mul_X hXp0
+... = p.degree : congr_arg _ (div_X_mul_X_add _)
+
+/-- An induction principle for polynomials, valued in Sort* instead of Prop. -/
+@[elab_as_eliminator] noncomputable def rec_on_horner
+  {M : polynomial R → Sort*} : Π (p : polynomial R),
+  M 0 →
+  (Π p a, coeff p 0 = 0 → a ≠ 0 → M p → M (p + C a)) →
+  (Π p, p ≠ 0 → M p → M (p * X)) →
+  M p
+| p := λ M0 MC MX,
+if hp : p = 0 then eq.rec_on hp.symm M0
+else
+have wf : degree (div_X p) < degree p,
+  from degree_div_X_lt hp,
+by rw [← div_X_mul_X_add p] at *;
+  exact
+  if hcp0 : coeff p 0 = 0
+  then by rw [hcp0, C_0, add_zero];
+    exact MX _ (λ h : div_X p = 0, by simpa [h, hcp0] using hp)
+      (rec_on_horner _ M0 MC MX)
+  else MC _ _ (coeff_mul_X_zero _) hcp0 (if hpX0 : div_X p = 0
+    then show M (div_X p * X), by rw [hpX0, zero_mul]; exact M0
+    else MX (div_X p) hpX0 (rec_on_horner _ M0 MC MX))
+using_well_founded {dec_tac := tactic.assumption}
+
+/--  A property holds for all polynomials of positive `degree` with coefficients in a semiring `R`
+if it holds for
+* `a * X`, with `a ∈ R`,
+* `p * X`, with `p ∈ R[X]`,
+* `p + a`, with `a ∈ R`, `p ∈ R[X]`,
+with appropriate restrictions on each term.
+
+See `nat_degree_ne_zero_induction_on` for a similar statement involving no explicit multiplication.
+ -/
+@[elab_as_eliminator] lemma degree_pos_induction_on
+  {P : polynomial R → Prop} (p : polynomial R) (h0 : 0 < degree p)
+  (hC : ∀ {a}, a ≠ 0 → P (C a * X))
+  (hX : ∀ {p}, 0 < degree p → P p → P (p * X))
+  (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
+rec_on_horner p
+  (λ h, by rw degree_zero at h; exact absurd h dec_trivial)
+  (λ p a _ _ ih h0,
+    have 0 < degree p,
+      from lt_of_not_ge (λ h, (not_lt_of_ge degree_C_le) $
+        by rwa [eq_C_of_degree_le_zero h, ← C_add] at h0),
+    hadd this (ih this))
+  (λ p _ ih h0',
+    if h0 : 0 < degree p
+    then hX h0 (ih h0)
+    else by rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at *;
+      exact hC (λ h : coeff p 0 = 0,
+        by simpa [h, nat.not_lt_zero] using h0'))
+  h0
+
+end semiring
+
+end polynomial
diff --git a/src/data/polynomial/integral_normalization.lean b/src/data/polynomial/integral_normalization.lean
index 8b04217f4f1b9..54cbd272f7636 100644
--- a/src/data/polynomial/integral_normalization.lean
+++ b/src/data/polynomial/integral_normalization.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.algebra_map
+import data.polynomial.degree.lemmas
 import data.polynomial.monic
 
 /-!
diff --git a/src/data/polynomial/monic.lean b/src/data/polynomial/monic.lean
index f587660f66549..7d193251a6687 100644
--- a/src/data/polynomial/monic.lean
+++ b/src/data/polynomial/monic.lean
@@ -56,7 +56,7 @@ begin
   rw [monic, leading_coeff, coeff_map],
   suffices : p.coeff (map f p).nat_degree = 1, simp [this],
   suffices : (map f p).nat_degree = p.nat_degree, rw this, exact hp,
-  rwa nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero _ _),
+  rwa nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f _)
 end
 
 lemma monic_mul_C_of_leading_coeff_mul_eq_one [nontrivial R] {b : R}
@@ -237,6 +237,34 @@ open function
 variables [semiring S] {f : R →+* S} (hf : injective f)
 include hf
 
+lemma degree_map_eq_of_injective (p : polynomial R) : degree (p.map f) = degree p :=
+if h : p = 0 then by simp [h]
+else degree_map_eq_of_leading_coeff_ne_zero _
+  (by rw [← f.map_zero]; exact mt hf.eq_iff.1
+    (mt leading_coeff_eq_zero.1 h))
+
+lemma degree_map' (p : polynomial R) :
+  degree (p.map f) = degree p :=
+p.degree_map_eq_of_injective hf
+
+lemma nat_degree_map' (p : polynomial R) :
+  nat_degree (p.map f) = nat_degree p :=
+nat_degree_eq_of_degree_eq (degree_map' hf p)
+
+lemma leading_coeff_map' (p : polynomial R) :
+  leading_coeff (p.map f) = f (leading_coeff p) :=
+begin
+  unfold leading_coeff,
+  rw [coeff_map, nat_degree_map' hf p],
+end
+
+lemma next_coeff_map (p : polynomial R) :
+  (p.map f).next_coeff = f p.next_coeff :=
+begin
+  unfold next_coeff,
+  rw nat_degree_map' hf,
+  split_ifs; simp
+end
 
 lemma leading_coeff_of_injective (p : polynomial R) :
   leading_coeff (p.map f) = f (leading_coeff p) :=
diff --git a/src/data/polynomial/reverse.lean b/src/data/polynomial/reverse.lean
index 9031da8f4d1ac..b96bb51098a69 100644
--- a/src/data/polynomial/reverse.lean
+++ b/src/data/polynomial/reverse.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import data.polynomial.erase_lead
-import data.polynomial.degree
+import data.polynomial.eval
 
 /-!
 # Reverse of a univariate polynomial
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index c71ca2c76f280..d3e0547587779 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker, Johan Commelin
 -/
 
-import data.polynomial.basic
 import data.polynomial.div
 import data.polynomial.algebra_map
-import data.set.finite
+import data.polynomial.degree.lemmas
 
 /-!
 # Theory of univariate polynomials
diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean
index fcb2baab5ab2a..6c8bae46bb857 100644
--- a/src/ring_theory/roots_of_unity.lean
+++ b/src/ring_theory/roots_of_unity.lean
@@ -903,10 +903,10 @@ begin
     (map (int.cast_ring_hom (zmod p)) P) with hle hunit,
   { exact not_lt_of_le hle habs },
   { replace hunit := degree_eq_zero_of_is_unit hunit,
-    rw degree_map_eq_of_leading_coeff_ne_zero _ _ at hunit,
-    { exact (ne_of_lt (minpoly.degree_pos (is_integral h hpos))).symm hunit },
+    rw degree_map_eq_of_leading_coeff_ne_zero (int.cast_ring_hom (zmod p)) _ at hunit,
+    { exact (minpoly.degree_pos (is_integral h hpos)).ne' hunit },
     simp only [Pmonic, ring_hom.eq_int_cast, monic.leading_coeff, int.cast_one, ne.def,
-      not_false_iff, one_ne_zero] },
+      not_false_iff, one_ne_zero] }
 end
 
 /-- If `m : ℕ` is coprime with `n`,