diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
index 1c8b9c16495ed..15d1844e601e4 100644
--- a/src/data/finsupp/basic.lean
+++ b/src/data/finsupp/basic.lean
@@ -156,7 +156,7 @@ by simp [← finsupp.support_eq_empty, finset.eq_empty_iff_forall_not_mem]
 lemma card_support_eq_zero {f : α →₀ M} : card f.support = 0 ↔ f = 0 :=
 by simp
 
-instance finsupp.decidable_eq [decidable_eq α] [decidable_eq M] : decidable_eq (α →₀ M) :=
+instance [decidable_eq α] [decidable_eq M] : decidable_eq (α →₀ M) :=
 assume f g, decidable_of_iff (f.support = g.support ∧ (∀a∈f.support, f a = g a)) ext_iff'.symm
 
 lemma finite_support (f : α →₀ M) : set.finite (function.support f) :=
@@ -2346,6 +2346,10 @@ lemma le_iff [canonically_ordered_add_monoid M] (f g : α →₀ M) :
 ⟨λ h s hs, h s,
 λ h s, if H : s ∈ f.support then h s H else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)⟩
 
+instance decidable_le [canonically_ordered_add_monoid M] [decidable_rel (@has_le.le M _)] :
+  decidable_rel (@has_le.le (α →₀ M) _) :=
+λ f g, decidable_of_iff _ (le_iff f g).symm
+
 @[simp] lemma add_eq_zero_iff [canonically_ordered_add_monoid M] (f g : α →₀ M) :
   f + g = 0 ↔ f = 0 ∧ g = 0 :=
 by simp [ext_iff, forall_and_distrib]
@@ -2377,9 +2381,6 @@ variable (α)
 lemma lt_wf : well_founded (@has_lt.lt (α →₀ ℕ) _) :=
 subrelation.wf (sum_id_lt_of_lt) $ inv_image.wf _ nat.lt_wf
 
-instance decidable_le : decidable_rel (@has_le.le (α →₀ ℕ) _) :=
-λ m n, by rw le_iff; apply_instance
-
 variable {α}
 
 @[simp] lemma nat_add_sub_cancel (f g : α →₀ ℕ) : f + g - g = f :=
diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean
index 7cd02f8f2ec28..1d2e6314bf481 100644
--- a/src/data/mv_polynomial/basic.lean
+++ b/src/data/mv_polynomial/basic.lean
@@ -371,15 +371,25 @@ lemma coeff_sum {X : Type*} (s : finset X) (f : X → mv_polynomial σ R) (m : 
 lemma monic_monomial_eq (m) : monomial m (1:R) = (m.prod $ λn e, X n ^ e : mv_polynomial σ R) :=
 by simp [monomial_eq]
 
-@[simp] lemma coeff_monomial (m n) (a) :
+@[simp] lemma coeff_monomial [decidable_eq σ] (m n) (a) :
   coeff m (monomial n a : mv_polynomial σ R) = if n = m then a else 0 :=
 single_apply
 
-@[simp] lemma coeff_C (m) (a) :
+@[simp] lemma coeff_C [decidable_eq σ] (m) (a) :
   coeff m (C a : mv_polynomial σ R) = if 0 = m then a else 0 :=
 single_apply
 
-lemma coeff_X_pow (i : σ) (m) (k : ℕ) :
+lemma coeff_one [decidable_eq σ] (m) :
+  coeff m (1 : mv_polynomial σ R) = if 0 = m then 1 else 0 :=
+coeff_C m 1
+
+@[simp] lemma coeff_zero_C (a) : coeff 0 (C a : mv_polynomial σ R) = a :=
+single_eq_same
+
+@[simp] lemma coeff_zero_one : coeff 0 (1 : mv_polynomial σ R) = 1 :=
+coeff_zero_C 1
+
+lemma coeff_X_pow [decidable_eq σ] (i : σ) (m) (k : ℕ) :
   coeff m (X i ^ k : mv_polynomial σ R) = if single i k = m then 1 else 0 :=
 begin
   have := coeff_monomial m (finsupp.single i k) (1:R),
@@ -388,7 +398,7 @@ begin
   exact pow_zero _
 end
 
-lemma coeff_X' (i : σ) (m) :
+lemma coeff_X' [decidable_eq σ] (i : σ) (m) :
   coeff m (X i : mv_polynomial σ R) = if single i 1 = m then 1 else 0 :=
 by rw [← coeff_X_pow, pow_one]
 
@@ -452,7 +462,7 @@ begin
   { rw [coeff_X', if_neg H, mul_zero] },
 end
 
-lemma coeff_mul_X' (m) (s : σ) (p : mv_polynomial σ R) :
+lemma coeff_mul_X' [decidable_eq σ] (m) (s : σ) (p : mv_polynomial σ R) :
   coeff m (p * X s) = if s ∈ m.support then coeff (m - single s 1) p else 0 :=
 begin
   nontriviality R,
@@ -529,7 +539,7 @@ lemma constant_coeff_X (i : σ) :
   constant_coeff (X i : mv_polynomial σ R) = 0 :=
 by simp [constant_coeff_eq]
 
-lemma constant_coeff_monomial (d : σ →₀ ℕ) (r : R) :
+lemma constant_coeff_monomial [decidable_eq σ] (d : σ →₀ ℕ) (r : R) :
   constant_coeff (monomial d r) = if d = 0 then r else 0 :=
 by rw [constant_coeff_eq, coeff_monomial]
 
diff --git a/src/data/mv_polynomial/pderiv.lean b/src/data/mv_polynomial/pderiv.lean
index d16f979572947..a81b17938a2b5 100644
--- a/src/data/mv_polynomial/pderiv.lean
+++ b/src/data/mv_polynomial/pderiv.lean
@@ -93,7 +93,8 @@ begin
   simp [mem_support_not_mem_vars_zero H h],
 end
 
-lemma pderiv_X {i j : σ} : pderiv i (X j : mv_polynomial σ R) = if i = j then 1 else 0 :=
+lemma pderiv_X [decidable_eq σ] {i j : σ} :
+  pderiv i (X j : mv_polynomial σ R) = if i = j then 1 else 0 :=
 begin
   dsimp [pderiv],
   erw finsupp.sum_single_index,
diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
index 52dba30131027..e35336bad2f99 100644
--- a/src/data/polynomial/field_division.lean
+++ b/src/data/polynomial/field_division.lean
@@ -224,7 +224,6 @@ else by rw [mod_def, mod_def, leading_coeff_map f, ← f.map_inv, ← map_C f,
 
 section
 open euclidean_domain
-local attribute [-instance] finsupp.finsupp.decidable_eq
 theorem gcd_map [field k] (f : R →+* k) :
   gcd (p.map f) (q.map f) = (gcd p q).map f :=
 gcd.induction p q (λ x, by simp_rw [map_zero, euclidean_domain.gcd_zero_left]) $ λ x y hx ih,
diff --git a/src/ring_theory/polynomial/homogeneous.lean b/src/ring_theory/polynomial/homogeneous.lean
index 52faedcd0531f..e752df851cfe0 100644
--- a/src/ring_theory/polynomial/homogeneous.lean
+++ b/src/ring_theory/polynomial/homogeneous.lean
@@ -114,6 +114,7 @@ lemma is_homogeneous_monomial (d : σ →₀ ℕ) (r : R) (n : ℕ) (hn : ∑ i
   is_homogeneous (monomial d r) n :=
 begin
   intros c hc,
+  classical,
   rw coeff_monomial at hc,
   split_ifs at hc with h,
   { subst c, exact hn },
diff --git a/src/ring_theory/power_series/basic.lean b/src/ring_theory/power_series/basic.lean
index 3ace0903b9be2..dc01dd9107231 100644
--- a/src/ring_theory/power_series/basic.lean
+++ b/src/ring_theory/power_series/basic.lean
@@ -114,10 +114,14 @@ lemma ext_iff {φ ψ : mv_power_series σ R} :
   φ = ψ ↔ (∀ (n : σ →₀ ℕ), coeff R n φ = coeff R n ψ) :=
 function.funext_iff
 
-lemma coeff_monomial (m n : σ →₀ ℕ) (a : R) :
+lemma monomial_def [decidable_eq σ] (n : σ →₀ ℕ) :
+  monomial R n = linear_map.std_basis R _ n :=
+by convert rfl -- unify the `decidable` arguments
+
+lemma coeff_monomial [decidable_eq σ] (m n : σ →₀ ℕ) (a : R) :
   coeff R m (monomial R n a) = if m = n then a else 0 :=
-by rw [coeff, monomial, linear_map.proj_apply, linear_map.std_basis_apply, function.update_apply,
-  pi.zero_apply]
+by rw [coeff, monomial_def, linear_map.proj_apply, linear_map.std_basis_apply,
+  function.update_apply, pi.zero_apply]
 
 @[simp] lemma coeff_monomial_same (n : σ →₀ ℕ) (a : R) :
   coeff R n (monomial R n a) = a :=
@@ -141,7 +145,7 @@ variables (m n : σ →₀ ℕ) (φ ψ : mv_power_series σ R)
 
 instance : has_one (mv_power_series σ R) := ⟨monomial R (0 : σ →₀ ℕ) 1⟩
 
-lemma coeff_one :
+lemma coeff_one [decidable_eq σ] :
   coeff R n (1 : mv_power_series σ R) = if n = 0 then 1 else 0 :=
 coeff_monomial _ _ _
 
@@ -287,7 +291,7 @@ variables {σ} {R}
 
 lemma monomial_zero_eq_C_apply (a : R) : monomial R (0 : σ →₀ ℕ) a = C σ R a := rfl
 
-lemma coeff_C (n : σ →₀ ℕ) (a : R) :
+lemma coeff_C [decidable_eq σ] (n : σ →₀ ℕ) (a : R) :
   coeff R n (C σ R a) = if n = 0 then a else 0 :=
 coeff_monomial _ _ _
 
@@ -297,11 +301,11 @@ coeff_monomial_same 0 a
 /-- The variables of the multivariate formal power series ring.-/
 def X (s : σ) : mv_power_series σ R := monomial R (single s 1) 1
 
-lemma coeff_X (n : σ →₀ ℕ) (s : σ) :
+lemma coeff_X [decidable_eq σ] (n : σ →₀ ℕ) (s : σ) :
   coeff R n (X s : mv_power_series σ R) = if n = (single s 1) then 1 else 0 :=
 coeff_monomial _ _ _
 
-lemma coeff_index_single_X (s t : σ) :
+lemma coeff_index_single_X [decidable_eq σ] (s t : σ) :
   coeff R (single t 1) (X s : mv_power_series σ R) = if t = s then 1 else 0 :=
 by { simp only [coeff_X, single_left_inj one_ne_zero], split_ifs; refl }
 
@@ -322,7 +326,7 @@ begin
   { rw [pow_succ', ih, nat.succ_eq_add_one, finsupp.single_add, X, monomial_mul_monomial, one_mul] }
 end
 
-lemma coeff_X_pow (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
+lemma coeff_X_pow [decidable_eq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
   coeff R m ((X s : mv_power_series σ R)^n) = if m = single s n then 1 else 0 :=
 by rw [X_pow_eq s n, coeff_monomial]
 
@@ -501,9 +505,9 @@ mv_polynomial.ext _ _ $ λ m,
 begin
   rw [coeff_trunc, coeff_one],
   split_ifs with H H' H',
-  { subst m, erw mv_polynomial.coeff_C 0, simp },
-  { symmetry, erw mv_polynomial.coeff_monomial, convert if_neg (ne.elim (ne.symm H')), },
-  { symmetry, erw mv_polynomial.coeff_monomial, convert if_neg _,
+  { subst m, simp },
+  { symmetry, rw mv_polynomial.coeff_one, exact if_neg (ne.symm H'), },
+  { symmetry, rw mv_polynomial.coeff_one, refine if_neg _,
     intro H', apply H, subst m, intro s, exact nat.zero_le _ }
 end
 
@@ -582,17 +586,21 @@ using_well_founded
 { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩],
   dec_tac := tactic.assumption }
 
-lemma coeff_inv_aux (n : σ →₀ ℕ) (a : R) (φ : mv_power_series σ R) :
+lemma coeff_inv_aux [decidable_eq σ] (n : σ →₀ ℕ) (a : R) (φ : mv_power_series σ R) :
   coeff R n (inv.aux a φ) = if n = 0 then a else
   - a * ∑ x in n.antidiagonal,
     if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 :=
-show inv.aux a φ n = _, by { rw inv.aux, refl }
+show inv.aux a φ n = _,
+begin
+  rw inv.aux,
+  convert rfl -- unify `decidable` instances
+end
 
 /-- A multivariate formal power series is invertible if the constant coefficient is invertible.-/
 def inv_of_unit (φ : mv_power_series σ R) (u : units R) : mv_power_series σ R :=
 inv.aux (↑u⁻¹) φ
 
-lemma coeff_inv_of_unit (n : σ →₀ ℕ) (φ : mv_power_series σ R) (u : units R) :
+lemma coeff_inv_of_unit [decidable_eq σ] (n : σ →₀ ℕ) (φ : mv_power_series σ R) (u : units R) :
   coeff R n (inv_of_unit φ u) = if n = 0 then ↑u⁻¹ else
   - ↑u⁻¹ * ∑ x in n.antidiagonal,
     if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv_of_unit φ u) else 0 :=
@@ -679,7 +687,7 @@ inv.aux (constant_coeff σ k φ)⁻¹ φ
 
 instance : has_inv (mv_power_series σ k) := ⟨mv_power_series.inv⟩
 
-lemma coeff_inv (n : σ →₀ ℕ) (φ : mv_power_series σ k) :
+lemma coeff_inv [decidable_eq σ] (n : σ →₀ ℕ) (φ : mv_power_series σ k) :
   coeff k n (φ⁻¹) = if n = 0 then (constant_coeff σ k φ)⁻¹ else
   - (constant_coeff σ k φ)⁻¹ * ∑ x in n.antidiagonal,
     if x.2 < n then coeff k x.1 φ * coeff k x.2 (φ⁻¹) else 0 :=
@@ -901,7 +909,7 @@ lemma coeff_C (n : ℕ) (a : R) :
   coeff R n (C R a : power_series R) = if n = 0 then a else 0 :=
 by rw [← monomial_zero_eq_C_apply, coeff_monomial]
 
-lemma coeff_zero_C (a : R) : coeff R 0 (C R a) = a :=
+@[simp] lemma coeff_zero_C (a : R) : coeff R 0 (C R a) = a :=
 by rw [← monomial_zero_eq_C_apply, coeff_monomial_same 0 a]
 
 lemma X_eq : (X : power_series R) = monomial R 1 1 := rfl
@@ -910,7 +918,7 @@ lemma coeff_X (n : ℕ) :
   coeff R n (X : power_series R) = if n = 1 then 1 else 0 :=
 by rw [X_eq, coeff_monomial]
 
-lemma coeff_zero_X : coeff R 0 (X : power_series R) = 0 :=
+@[simp] lemma coeff_zero_X : coeff R 0 (X : power_series R) = 0 :=
 by rw [coeff, finsupp.single_zero, X, mv_power_series.coeff_zero_X]
 
 @[simp] lemma coeff_one_X : coeff R 1 (X : power_series R) = 1 :=
@@ -929,9 +937,7 @@ by rw [coeff_X_pow, if_pos rfl]
 
 @[simp] lemma coeff_one (n : ℕ) :
   coeff R n (1 : power_series R) = if n = 0 then 1 else 0 :=
-calc coeff R n (1 : power_series R) = _ : mv_power_series.coeff_one _
-    ... = if n = 0 then 1 else 0 :
-by { simp only [finsupp.single_eq_zero], split_ifs; refl }
+coeff_C n 1
 
 lemma coeff_zero_one : coeff R 0 (1 : power_series R) = 1 :=
 coeff_zero_C 1
@@ -1554,7 +1560,7 @@ begin
 end
 
 /-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise.-/
-lemma order_monomial (n : ℕ) (a : R) :
+lemma order_monomial (n : ℕ) (a : R) [decidable (a = 0)] :
   order (monomial R n a) = if a = 0 then ⊤ else n :=
 begin
   split_ifs with h,