diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean
index 03f7786c8e76b..13bfeb47bd643 100644
--- a/src/ring_theory/ideal/operations.lean
+++ b/src/ring_theory/ideal/operations.lean
@@ -1099,7 +1099,8 @@ theorem mem_image_of_mem_map_of_surjective {I : ideal R} {y}
 submodule.span_induction H (λ _, id) ⟨0, I.zero_mem, f.map_zero⟩
 (λ y1 y2 ⟨x1, hx1i, hxy1⟩ ⟨x2, hx2i, hxy2⟩,
   ⟨x1 + x2, I.add_mem hx1i hx2i, hxy1 ▸ hxy2 ▸ f.map_add _ _⟩)
-(λ c y ⟨x, hxi, hxy⟩, let ⟨d, hdc⟩ := hf c in ⟨d • x, I.smul_mem _ hxi, hdc ▸ hxy ▸ f.map_mul _ _⟩)
+(λ c y ⟨x, hxi, hxy⟩,
+  let ⟨d, hdc⟩ := hf c in ⟨d * x, I.mul_mem_left _ hxi, hdc ▸ hxy ▸ f.map_mul _ _⟩)
 
 lemma mem_map_iff_of_surjective {I : ideal R} {y} :
   y ∈ map f I ↔ ∃ x, x ∈ I ∧ f x = y :=
diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean
index 5095f47c1a831..a56ef1f4513ac 100644
--- a/src/ring_theory/jacobson.lean
+++ b/src/ring_theory/jacobson.lean
@@ -244,8 +244,8 @@ begin
     { rw [ideal.jacobson, mem_Inf],
       intros J hJ,
       by_cases y ∈ J,
-      { exact J.smul_mem x h },
-      { exact (mul_comm y x) ▸ J.smul_mem y ((mem_Inf.1 hx) ⟨hJ.left, ⟨hJ.right, h⟩⟩) } },
+      { exact J.mul_mem_left x h },
+      { exact J.mul_mem_right y ((mem_Inf.1 hx) ⟨hJ.left, ⟨hJ.right, h⟩⟩) } },
     rw hP at hxy,
     cases hP'.mem_or_mem hxy with hxy hxy,
     { exact hxy },
diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean
index cb9c39882fdf4..0ebdeec05312f 100644
--- a/src/ring_theory/polynomial/basic.lean
+++ b/src/ring_theory/polynomial/basic.lean
@@ -399,7 +399,7 @@ begin
     { exact λ f g hf hg n, by simp [I.add_mem (hf n) (hg n)] },
     { refine λ f g hg n, _,
       rw [smul_eq_mul, coeff_mul],
-      exact I.sum_mem (λ c hc, I.smul_mem (f.coeff c.fst) (hg c.snd)) } },
+      exact I.sum_mem (λ c hc, I.mul_mem_left (f.coeff c.fst) (hg c.snd)) } },
   { intros hf,
     rw ← sum_monomial_eq f,
     refine (I.map C : ideal R[X]).sum_mem (λ n hn, _),
@@ -558,8 +558,8 @@ lemma eq_zero_of_constant_mem_of_maximal (hR : is_field R)
 begin
   refine classical.by_contradiction (λ hx0, hI.ne_top ((eq_top_iff_one I).2 _)),
   obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0,
-  convert I.smul_mem (C y) hx,
-  rw [smul_eq_mul, ← C.map_mul, mul_comm y x, hy, ring_hom.map_one],
+  convert I.mul_mem_left (C y) hx,
+  rw [← C.map_mul, mul_comm y x, hy, ring_hom.map_one],
 end
 
 /-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
@@ -982,7 +982,7 @@ begin
     { exact λ f g hf hg n, by simp [I.add_mem (hf n) (hg n)] },
     { refine λ f g hg n, _,
       rw [smul_eq_mul, coeff_mul],
-      exact I.sum_mem (λ c hc, I.smul_mem (f.coeff c.fst) (hg c.snd)) } },
+      exact I.sum_mem (λ c hc, I.mul_mem_left (f.coeff c.fst) (hg c.snd)) } },
   { intros hf,
     rw as_sum f,
     suffices : ∀ m ∈ f.support, monomial m (coeff m f) ∈