diff --git a/src/data/polynomial/algebra_map.lean b/src/data/polynomial/algebra_map.lean
index 107bc4751dad4..495405d4a41b4 100644
--- a/src/data/polynomial/algebra_map.lean
+++ b/src/data/polynomial/algebra_map.lean
@@ -14,9 +14,6 @@ We promote `eval₂` to an algebra hom in `aeval`.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean
index 50b4d19f1f832..f498ee4c3ae0c 100644
--- a/src/data/polynomial/basic.lean
+++ b/src/data/polynomial/basic.lean
@@ -16,8 +16,6 @@ In this file, we define `polynomial`, provide basic instances, and prove an `ext
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
 
 /-- `polynomial R` is the type of univariate polynomials over `R`.
 
@@ -101,17 +99,11 @@ coeff_monomial
 
 @[simp] lemma coeff_one_zero : coeff (1 : polynomial R) 0 = 1 := coeff_monomial
 
+@[simp] lemma coeff_X_one : coeff (X : polynomial R) 1 = 1 := coeff_monomial
 
-instance [has_repr R] : has_repr (polynomial R) :=
-⟨λ p, if p = 0 then "0"
-  else (p.support.sort (≤)).foldr
-    (λ n a, a ++ (if a = "" then "" else " + ") ++
-      if n = 0
-        then "C (" ++ repr (coeff p n) ++ ")"
-        else if n = 1
-          then if (coeff p n) = 1 then "X" else "C (" ++ repr (coeff p n) ++ ") * X"
-          else if (coeff p n) = 1 then "X ^ " ++ repr n
-            else "C (" ++ repr (coeff p n) ++ ") * X ^ " ++ repr n) ""⟩
+@[simp] lemma coeff_X_zero : coeff (X : polynomial R) 0 = 0 := coeff_monomial
+
+lemma coeff_X : coeff (X : polynomial R) n = if 1 = n then 1 else 0 := coeff_monomial
 
 theorem ext_iff {p q : polynomial R} : p = q ↔ ∀ n, coeff p n = coeff q n :=
 ⟨λ h n, h ▸ rfl, finsupp.ext⟩
@@ -126,7 +118,6 @@ by rw [←one_smul R p, ←h, zero_smul]
 
 end semiring
 
-
 section ring
 variables [ring R]
 
@@ -139,23 +130,38 @@ lemma coeff_sub (p q : polynomial R) (n : ℕ) : coeff (p - q) n = coeff p n - c
 
 end ring
 
-
-section comm_semiring
-variables [comm_semiring R]
-
-instance : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
-
-end comm_semiring
+instance [comm_semiring R] : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
+instance [comm_ring R] : comm_ring (polynomial R) := add_monoid_algebra.comm_ring
 
 section nonzero_semiring
 
-variables [semiring R] [nontrivial R] {p q : polynomial R}
+variables [semiring R] [nontrivial R]
 instance : nontrivial (polynomial R) :=
 begin
   refine nontrivial_of_ne 0 1 _, intro h,
   have := coeff_zero 0, revert this, rw h, simp,
 end
 
+lemma X_ne_zero : (X : polynomial R) ≠ 0 :=
+mt (congr_arg (λ p, coeff p 1)) (by simp)
+
 end nonzero_semiring
 
+section repr
+variables [semiring R]
+local attribute [instance, priority 100] classical.prop_decidable
+
+instance [has_repr R] : has_repr (polynomial R) :=
+⟨λ p, if p = 0 then "0"
+  else (p.support.sort (≤)).foldr
+    (λ n a, a ++ (if a = "" then "" else " + ") ++
+      if n = 0
+        then "C (" ++ repr (coeff p n) ++ ")"
+        else if n = 1
+          then if (coeff p n) = 1 then "X" else "C (" ++ repr (coeff p n) ++ ") * X"
+          else if (coeff p n) = 1 then "X ^ " ++ repr n
+            else "C (" ++ repr (coeff p n) ++ ") * X ^ " ++ repr n) ""⟩
+
+end repr
+
 end polynomial
diff --git a/src/data/polynomial/coeff.lean b/src/data/polynomial/coeff.lean
index 6c741e4d101dd..ffe52898e3a2f 100644
--- a/src/data/polynomial/coeff.lean
+++ b/src/data/polynomial/coeff.lean
@@ -15,7 +15,6 @@ The theorems include formulas for computing coefficients, such as
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
@@ -24,12 +23,10 @@ namespace polynomial
 universes u v
 variables {R : Type u} {S : Type v} {a b : R} {n m : ℕ}
 
-section semiring
 variables [semiring R] {p q r : polynomial R}
 
 section coeff
 
-@[simp, priority 990]
 lemma coeff_one (n : ℕ) : coeff (1 : polynomial R) n = if 0 = n then 1 else 0 :=
 coeff_monomial
 
@@ -42,11 +39,6 @@ lemma coeff_sum [semiring S] (n : ℕ) (f : ℕ → R → polynomial S) :
 @[simp] lemma coeff_smul (p : polynomial R) (r : R) (n : ℕ) :
 coeff (r • p) n = r * coeff p n := finsupp.smul_apply
 
--- TODO: bundle into a def instead of an instance?
-instance coeff.is_add_monoid_hom {n : ℕ} : is_add_monoid_hom (λ p : polynomial R, p.coeff n) :=
-{ map_add  := λ p q, coeff_add p q n,
-  map_zero := coeff_zero _ }
-
 variable (R)
 /-- The nth coefficient, as a linear map. -/
 def lcoeff (n : ℕ) : polynomial R →ₗ[R] R :=
@@ -81,9 +73,11 @@ end
 @[simp] lemma mul_coeff_zero (p q : polynomial R) : coeff (p * q) 0 = coeff p 0 * coeff q 0 :=
 by simp [coeff_mul]
 
-@[simp] lemma coeff_mul_X_zero (p : polynomial R) : coeff (p * X) 0 = 0 :=
-by rw [coeff_mul, nat.antidiagonal_zero];
-simp only [polynomial.coeff_X_zero, finset.sum_singleton, mul_zero]
+lemma coeff_mul_X_zero (p : polynomial R) : coeff (p * X) 0 = 0 :=
+by simp
+
+lemma coeff_X_mul_zero (p : polynomial R) : coeff (X * p) 0 = 0 :=
+by simp
 
 lemma coeff_C_mul_X (x : R) (k n : ℕ) :
   coeff (C x * X^k : polynomial R) n = if n = k then x else 0 :=
@@ -123,10 +117,15 @@ begin
     ... = a • X^n  : by rw monomial_one_eq_X_pow
 end
 
-@[simp] lemma coeff_X_pow (k n : ℕ) :
+lemma coeff_X_pow (k n : ℕ) :
   coeff (X^k : polynomial R) n = if n = k then 1 else 0 :=
 by rw [← monomial_one_eq_X_pow]; simp [monomial, single, eq_comm, coeff]; congr
 
+@[simp]
+lemma coeff_X_pow_self (n : ℕ) :
+  coeff (X^n : polynomial R) n = 1 :=
+by simp [coeff_X_pow]
+
 theorem coeff_mul_X_pow (p : polynomial R) (n d : ℕ) :
   coeff (p * polynomial.X ^ n) (d + n) = coeff p d :=
 begin
@@ -147,7 +146,4 @@ ext $ λ k, (coeff_mul_X_pow p n k).symm.trans $ ext_iff.1 H (k+n)
 
 end coeff
 
-end semiring
-
-
 end polynomial
diff --git a/src/data/polynomial/degree.lean b/src/data/polynomial/degree.lean
index 6fc114d965f03..c5df2ccfe198f 100644
--- a/src/data/polynomial/degree.lean
+++ b/src/data/polynomial/degree.lean
@@ -20,8 +20,6 @@ Some of the main results include
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
@@ -464,7 +462,7 @@ have h : leading_coeff (X : polynomial R) * leading_coeff (X ^ n) ≠ 0,
 by rw [pow_succ, degree_mul' h, degree_X, degree_X_pow, add_comm]; refl
 
 theorem not_is_unit_X : ¬ is_unit (X : polynomial R) :=
-λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by erw [← coeff_one_zero, ← hgf, coeff_mul_X_zero]
+λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by { rw [← coeff_one_zero, ← hgf], simp }
 
 end nonzero_semiring
 
diff --git a/src/data/polynomial/degree/basic.lean b/src/data/polynomial/degree/basic.lean
index ea1aa5986d7f6..6c4eadcc82538 100644
--- a/src/data/polynomial/degree/basic.lean
+++ b/src/data/polynomial/degree/basic.lean
@@ -15,13 +15,11 @@ The definitions include
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
 namespace polynomial
-universes u v --w x y z
+universes u v
 variables {R : Type u} {S : Type v} {a b : R} {n m : ℕ}
 
 section semiring
diff --git a/src/data/polynomial/derivative.lean b/src/data/polynomial/derivative.lean
index 0c3fa3c604b66..a71ed17d3a2db 100644
--- a/src/data/polynomial/derivative.lean
+++ b/src/data/polynomial/derivative.lean
@@ -14,8 +14,6 @@ import data.polynomial.field_division
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
diff --git a/src/data/polynomial/div.lean b/src/data/polynomial/div.lean
index e701f6bd217ad..fcda31c899e95 100644
--- a/src/data/polynomial/div.lean
+++ b/src/data/polynomial/div.lean
@@ -18,8 +18,6 @@ We also define `root_multiplicity`.
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
--- local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
@@ -59,7 +57,7 @@ def div_X (p : polynomial R) : polynomial R :=
   mem_support_to_fun := λ n,
     suffices (∃ (a : ℕ), (¬coeff p a = 0 ∧ a > 0) ∧ a - 1 = n) ↔
       ¬coeff p (n + 1) = 0,
-    by simpa [finset.mem_def.symm, apply_eq_coeff],
+    by simpa [finset.mem_def.symm],
     ⟨λ ⟨a, ha⟩, by rw [← ha.2, nat.sub_add_cancel ha.1.2]; exact ha.1.1,
       λ h, ⟨n + 1, ⟨h, nat.succ_pos _⟩, nat.succ_sub_one _⟩⟩ }
 
diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
index 94f33a4341c03..689e846c8b2a7 100644
--- a/src/data/polynomial/eval.lean
+++ b/src/data/polynomial/eval.lean
@@ -422,10 +422,8 @@ by rw [is_root.def, eval_sub, eval_X, eval_C, sub_eq_zero_iff_eq, eq_comm]
 
 end ring
 
-
 section comm_ring
 variables [comm_ring R] {p q : polynomial R}
-instance : comm_ring (polynomial R) := add_monoid_algebra.comm_ring
 
 instance eval₂.is_ring_hom {S} [comm_ring S]
   (f : R →+* S) {x : S} : is_ring_hom (eval₂ f x) :=
diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
index 537f3c6575730..aeb41504be8db 100644
--- a/src/data/polynomial/field_division.lean
+++ b/src/data/polynomial/field_division.lean
@@ -17,8 +17,6 @@ This file starts looking like the ring theory of $ R[X] $
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
@@ -26,9 +24,6 @@ namespace polynomial
 universes u v w y z
 variables {R : Type u} {S : Type v} {k : Type y} {A : Type z} {a b : R} {n : ℕ}
 
-
-
-
 section field
 variables [field R] {p q : polynomial R}
 
diff --git a/src/data/polynomial/identities.lean b/src/data/polynomial/identities.lean
index c492c55015ce7..798fa6da71325 100644
--- a/src/data/polynomial/identities.lean
+++ b/src/data/polynomial/identities.lean
@@ -12,9 +12,6 @@ The main def is `binom_expansion`.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
@@ -24,12 +21,10 @@ universes u v w x y z
 variables {R : Type u} {S : Type v} {T : Type w} {ι : Type x} {k : Type y} {A : Type z}
   {a b : R} {m n : ℕ}
 
-
-
 section identities
 
 /- @TODO: pow_add_expansion and pow_sub_pow_factor are not specific to polynomials.
-  These belong somewhere else. But not in group_power because they depend on tactic.ring
+  These belong somewhere else. But not in group_power because they depend on tactic.ring_exp
 
 Maybe use data.nat.choose to prove it.
  -/
diff --git a/src/data/polynomial/induction.lean b/src/data/polynomial/induction.lean
index dc2253a3e3331..2f360982314df 100644
--- a/src/data/polynomial/induction.lean
+++ b/src/data/polynomial/induction.lean
@@ -12,9 +12,6 @@ The main results are `induction_on` and `as_sum`.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
@@ -89,7 +86,7 @@ end coeff
 -- TODO find a home (this file)
 @[simp] lemma finset_sum_coeff (s : finset ι) (f : ι → polynomial R) (n : ℕ) :
   coeff (∑ b in s, f b) n = ∑ b in s, coeff (f b) n :=
-(s.sum_hom (λ q : polynomial R, q.coeff n)).symm
+(s.sum_hom (λ q : polynomial R, lcoeff R n q)).symm
 
 lemma as_sum (p : polynomial R) :
   p = ∑ i in range (p.nat_degree + 1), C (p.coeff i) * X^i :=
diff --git a/src/data/polynomial/monic.lean b/src/data/polynomial/monic.lean
index 0fe0900a45fec..222c048484ef5 100644
--- a/src/data/polynomial/monic.lean
+++ b/src/data/polynomial/monic.lean
@@ -1,14 +1,12 @@
-import data.polynomial.algebra_map
-import algebra.gcd_domain
-import tactic.omega
-import tactic.ring
-
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 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 algebra.gcd_domain
+import tactic.ring
+import tactic.omega
 
 /-!
 # Theory of monic polynomials
@@ -21,8 +19,6 @@ and then define `integral_normalization`, which relate arbitrary polynomials to
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
diff --git a/src/data/polynomial/monomial.lean b/src/data/polynomial/monomial.lean
index 063c0f8d6ee5d..045429e62c303 100644
--- a/src/data/polynomial/monomial.lean
+++ b/src/data/polynomial/monomial.lean
@@ -12,22 +12,20 @@ Preparatory lemmas for degree_basic.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
 namespace polynomial
+
 universes u
 variables {R : Type u} {a b : R} {m n : ℕ}
-
-section semiring
 variables [semiring R] {p q r : polynomial R}
 
-section C
-/-- `C a` is the constant polynomial `a`. -/
+/--
+`C a` is the constant polynomial `a`.
+`C` is provided as a ring homomorphism.
+-/
 def C : R →+* polynomial R := add_monoid_algebra.algebra_map' (ring_hom.id R)
 
 @[simp] lemma monomial_zero_left (a : R) : monomial 0 a = C a := rfl
@@ -44,9 +42,6 @@ lemma C_add : C (a + b) = C a + C b := C.map_add a b
 
 @[simp] lemma C_bit1 : C (bit1 a) = bit1 (C a) := by simp [bit1, C_bit0]
 
-instance C.is_semiring_hom : is_semiring_hom (C : R → polynomial R) :=
-C.is_semiring_hom
-
 lemma C_pow : C (a ^ n) = C a ^ n := C.map_pow a n
 
 @[simp]
@@ -57,15 +52,6 @@ C.map_nat_cast n
 lemma sum_C_index {a} {β} [add_comm_monoid β] {f : ℕ → R → β} (h : f 0 0 = 0) :
   (C a).sum f = f 0 a :=
 sum_single_index h
-end C
-
-section coeff
-
-@[simp] lemma coeff_X_one : coeff (X : polynomial R) 1 = 1 := coeff_monomial
-
-@[simp] lemma coeff_X_zero : coeff (X : polynomial R) 0 = 0 := coeff_monomial
-
-lemma coeff_X : coeff (X : polynomial R) n = if 1 = n then 1 else 0 := coeff_monomial
 
 lemma coeff_C : coeff (C a) n = ite (n = 0) a 0 :=
 by { convert coeff_monomial using 2, simp [eq_comm], }
@@ -83,24 +69,4 @@ lemma single_eq_C_mul_X : ∀{n}, monomial n a = C a * X^n
     ... = (C a * X^n) * X : by rw [single_eq_C_mul_X]
     ... = C a * X^(n+1) : by simp only [pow_add, mul_assoc, pow_one]
 
-end coeff
-
-end semiring
-
-
-
-section nonzero_semiring
-
-variables [semiring R] [nontrivial R] {p q : polynomial R}
-lemma X_ne_zero : (X : polynomial R) ≠ 0 :=
-mt (congr_arg (λ p, coeff p 1)) (by simp)
-
-end nonzero_semiring
-
-section ring
-variables [ring R]
-
-
-end ring
-
 end polynomial
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index fe3df43855422..072004c4612b3 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -17,8 +17,6 @@ This file starts looking like the ring theory of $ R[X] $
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
@@ -195,8 +193,6 @@ then if h : (X : polynomial R) ^ n - C a = 0
 else by rw [← with_bot.coe_le_coe, ← degree_X_pow_sub_C (nat.pos_of_ne_zero hn) a];
   exact card_roots (X_pow_sub_C_ne_zero (nat.pos_of_ne_zero hn) a)
 
-
-
 lemma coeff_comp_degree_mul_degree (hqd0 : nat_degree q ≠ 0) :
   coeff (p.comp q) (nat_degree p * nat_degree q) =
   leading_coeff p * leading_coeff q ^ nat_degree p :=
@@ -210,7 +206,6 @@ calc coeff (p.comp q) (nat_degree p * nat_degree q)
     assume b hbs hbp,
     have hq0 : q ≠ 0, from λ hq0, hqd0 (by rw [hq0, nat_degree_zero]),
     have : coeff p b ≠ 0, rwa finsupp.mem_support_iff at hbs,
-    dsimp [apply_eq_coeff],
     refine coeff_eq_zero_of_degree_lt _,
     rw [degree_mul], erw degree_C this,
     rw [degree_pow, zero_add, degree_eq_nat_degree hq0,