chore(ring_theory/ideal/basic): Make an argument to mul_mem_{left,rig…

…ht} explicit (#5611)

Before this change, the lemmas with result `a * b ∈ I` did not have enough explicit arguments to determine both `a` and `b`, such as `I.mul_mem_left hb`.

This resulted in callers using `show`, `@`, or sometimes ignoring the API and using `smul_mem` which does have appropriate argument explicitness. These callers have been cleaned up accordingly.

src/algebraic_geometry/prime_spectrum.lean

@@ -280,9 +280,7 @@ begin
     rcases hs with ⟨s, hs1, hs2⟩,
     apply (ideal.is_prime.mem_or_mem (by apply_instance) _).resolve_left hs2,
     apply h,
-    split,
-    { exact ideal.mul_mem_left _ hr },
-    { exact ideal.mul_mem_right _ hs1 } },
+    exact ⟨I.mul_mem_left _ hr, J.mul_mem_right _ hs1⟩ },
   { rintro (h|h),
     all_goals
     { rw mem_zero_locus at h ⊢,

src/data/padics/ring_homs.lean

@@ -237,9 +237,7 @@ def to_zmod_hom (v : ℕ) (f : ℤ_[p] → ℕ) (f_spec : ∀ x, x - f x ∈ (id
     rw [f_congr (x * y) _ (f x * f y), cast_mul],
     { exact f_spec _ },
     { let I : ideal ℤ_[p] := ideal.span {v},
-      have A : x * (y - f y) ∈ I := I.mul_mem_left (f_spec _),
-      have B : (x - f x) * (f y) ∈ I := I.mul_mem_right (f_spec _),
-      convert I.add_mem A B,
+      convert I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right (f y) (f_spec x)),
       rw cast_mul,
       ring, }
   end, }

src/ring_theory/discrete_valuation_ring.lean

@@ -246,7 +246,7 @@ begin
   have ex : ∃ n : ℕ, p ^ n ∈ I,
   { obtain ⟨n, u, rfl⟩ := H hx0,
     refine ⟨n, _⟩,
-    simpa only [units.mul_inv_cancel_right] using @ideal.mul_mem_right _ _ I _ ↑u⁻¹ hxI, },
+    simpa only [units.mul_inv_cancel_right] using I.mul_mem_right ↑u⁻¹ hxI, },
   constructor,
   use p ^ (nat.find ex),
   show I = ideal.span _,
@@ -258,7 +258,7 @@ begin
     simp only [mem_span_singleton, is_unit_unit, is_unit.dvd_mul_right],
     apply pow_dvd_pow,
     apply nat.find_min',
-    simpa only [units.mul_inv_cancel_right] using @ideal.mul_mem_right _ _ I _ ↑u⁻¹ hr, },
+    simpa only [units.mul_inv_cancel_right] using I.mul_mem_right ↑u⁻¹ hr, },
   { erw submodule.span_singleton_le_iff_mem,
     exact nat.find_spec ex, },
 end

src/ring_theory/ideal/basic.lean

@@ -49,9 +49,13 @@ lemma add_mem_iff_right : a ∈ I → (a + b ∈ I ↔ b ∈ I) := I.add_mem_iff
 
 protected lemma sub_mem : a ∈ I → b ∈ I → a - b ∈ I := I.sub_mem
 
-lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem _
+variables (a)
+lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem a
+variables {a}
 
-lemma mul_mem_right (h : a ∈ I) : a * b ∈ I := mul_comm b a ▸ I.mul_mem_left h
+variables (b)
+lemma mul_mem_right (h : a ∈ I) : a * b ∈ I := mul_comm b a ▸ I.mul_mem_left b h
+variables {b}
 end ideal
 
 variables {a b : α}
@@ -68,7 +72,7 @@ theorem eq_top_of_unit_mem
 eq_top_iff.2 $ λ z _, calc
     z = z * (y * x) : by simp [h]
   ... = (z * y) * x : eq.symm $ mul_assoc z y x
-  ... ∈ I : I.mul_mem_left hx
+  ... ∈ I : I.mul_mem_left _ hx
 
 theorem eq_top_of_is_unit_mem {x} (hx : x ∈ I) (h : is_unit x) : I = ⊤ :=
 let ⟨y, hy⟩ := is_unit_iff_exists_inv'.1 h in eq_top_of_unit_mem I x y hx hy
@@ -83,10 +87,10 @@ not_congr I.eq_top_iff_one
 @[simp]
 theorem unit_mul_mem_iff_mem {x y : α} (hy : is_unit y) : y * x ∈ I ↔ x ∈ I :=
 begin
-  refine ⟨λ h, _, λ h,  I.smul_mem y h⟩,
+  refine ⟨λ h, _, λ h, I.mul_mem_left y h⟩,
   obtain ⟨y', hy'⟩ := is_unit_iff_exists_inv.1 hy,
-  have := I.smul_mem y' h,
-  rwa [smul_eq_mul, ← mul_assoc, mul_comm y' y, hy', one_mul] at this,
+  have := I.mul_mem_left y' h,
+  rwa [← mul_assoc, mul_comm y' y, hy', one_mul] at this,
 end
 
 @[simp]
@@ -227,9 +231,9 @@ end
 theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime :=
 ⟨H.1, λ x y hxy, or_iff_not_imp_left.2 $ λ hx, begin
   cases H.exists_inv hx with z hz,
-  have := I.mul_mem_left hz,
+  have := I.mul_mem_left _ hz,
   rw [mul_sub, mul_one, mul_comm, mul_assoc, sub_eq_add_neg] at this,
-  exact I.neg_mem_iff.1 ((I.add_mem_iff_right $ I.mul_mem_left hxy).1 this)
+  exact I.neg_mem_iff.1 ((I.add_mem_iff_right $ I.mul_mem_left _ hxy).1 this)
 end⟩
 
 @[priority 100] -- see Note [lower instance priority]
@@ -293,7 +297,7 @@ instance (I : ideal α) : has_mul I.quotient :=
 ⟨λ a b, quotient.lift_on₂' a b (λ a b, submodule.quotient.mk (a * b)) $
  λ a₁ a₂ b₁ b₂ h₁ h₂, quot.sound $ begin
   refine calc a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ : _
-  ... ∈ I : I.add_mem (I.mul_mem_left h₁) (I.mul_mem_right h₂),
+  ... ∈ I : I.add_mem (I.mul_mem_left _ h₁) (I.mul_mem_right _ h₂),
   rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁]
  end⟩
 
@@ -380,11 +384,11 @@ begin
   split,
   { intro h,
     rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩,
-    exact hxy (ideal.quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left h)) },
+    exact hxy (ideal.quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h)) },
   { intros J x hIJ hxnI hxJ,
     rcases hqf.mul_inv_cancel (mt ideal.quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩,
     rw [← zero_add (1 : α), ← sub_self (x * y), sub_add],
-    refine J.sub_mem (J.mul_mem_right hxJ) (hIJ (ideal.quotient.eq.1 hy)) }
+    refine J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (ideal.quotient.eq.1 hy)) }
 end
 
 /-- The quotient of a ring by an ideal is a field iff the ideal is maximal. -/
@@ -453,7 +457,7 @@ begin
   rw eq_bot_iff,
   intros r hr,
   by_cases H : r = 0, {simpa},
-  simpa [H, h1] using submodule.smul_mem I r⁻¹ hr,
+  simpa [H, h1] using I.mul_mem_left r⁻¹ hr,
 end
 
 lemma eq_bot_of_prime {K : Type u} [field K] (I : ideal K) [h : I.is_prime] :
@@ -470,9 +474,9 @@ variables (ι : Type v)
 /-- `I^n` as an ideal of `R^n`. -/
 def pi : ideal (ι → α) :=
 { carrier := { x | ∀ i, x i ∈ I },
-  zero_mem' := λ i, submodule.zero_mem _,
-  add_mem' := λ a b ha hb i, submodule.add_mem _ (ha i) (hb i),
-  smul_mem' := λ a b hb i, ideal.mul_mem_left _ (hb i) }
+  zero_mem' := λ i, I.zero_mem,
+  add_mem' := λ a b ha hb i, I.add_mem (ha i) (hb i),
+  smul_mem' := λ a b hb i, I.mul_mem_left (a i) (hb i) }
 
 lemma mem_pi (x : ι → α) : x ∈ I.pi ι ↔ ∀ i, x i ∈ I := iff.rfl
 
@@ -493,7 +497,7 @@ begin
       simpa only [neg_sub] using hm i },
     rw [←ideal.add_mem_iff_left (I.pi ι) this, sub_eq_add_neg, add_comm, ←add_assoc, ←smul_add,
       sub_add_cancel, ←sub_eq_add_neg, ←sub_smul, ideal.mem_pi],
-    exact λ i, ideal.mul_mem_right _ hc },
+    exact λ i, I.mul_mem_right _ hc },
   all_goals { rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ <|> rintro ⟨a⟩,
     simp only [(•), submodule.quotient.quot_mk_eq_mk, ideal.quotient.mk_eq_mk],
     change ideal.quotient.mk _ _ = ideal.quotient.mk _ _,
@@ -528,7 +532,7 @@ lemma map_pi {ι} [fintype ι] {ι' : Type w} (x : ι → α) (hi : ∀ i, x i 
 begin
   rw pi_eq_sum_univ x,
   simp only [finset.sum_apply, smul_eq_mul, linear_map.map_sum, pi.smul_apply, linear_map.map_smul],
-  exact submodule.sum_mem _ (λ j hj, ideal.mul_mem_right _ (hi j))
+  exact I.sum_mem (λ j hj, I.mul_mem_right _ (hi j))
 end
 
 end pi
@@ -566,7 +570,7 @@ begin
     rw submodule.mem_bot at ne_zero,
     obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero,
     rw [lt_top_iff_ne_top, ne.def, ideal.eq_top_iff_one, ← hy] at lt_top,
-    exact lt_top (ideal.mul_mem_right _ mem), }
+    exact lt_top (I.mul_mem_right _ mem), }
 end
 
 lemma not_is_field_iff_exists_prime [nontrivial R] :
@@ -684,7 +688,7 @@ begin
   { intros I x hI hx H,
     erw not_not at hx,
     rcases hx with ⟨u,rfl⟩,
-    simpa using I.smul_mem ↑u⁻¹ H }
+    simpa using I.mul_mem_left ↑u⁻¹ H }
 end
 
 lemma maximal_ideal_unique :

src/ring_theory/ideal/operations.lean

@@ -90,10 +90,10 @@ theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N)
 theorem mem_smul_span_singleton {I : ideal R} {m : M} {x : M} :
   x ∈ I • span R ({m} : set M) ↔ ∃ y ∈ I, y • m = x :=
 ⟨λ hx, smul_induction_on hx
-  (λ r hri n hnm, let ⟨s, hs⟩ := mem_span_singleton.1 hnm in ⟨r * s, I.mul_mem_right hri, hs ▸ mul_smul r s m⟩)
+  (λ r hri n hnm, let ⟨s, hs⟩ := mem_span_singleton.1 hnm in ⟨r * s, I.mul_mem_right _ hri, hs ▸ mul_smul r s m⟩)
   ⟨0, I.zero_mem, by rw [zero_smul]⟩
   (λ m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩, ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩)
-  (λ c r ⟨y, hyi, hy⟩, ⟨c * y, I.mul_mem_left hyi, by rw [mul_smul, hy]⟩),
+  (λ c r ⟨y, hyi, hy⟩, ⟨c * y, I.mul_mem_left _ hyi, by rw [mul_smul, hy]⟩),
 λ ⟨y, hyi, hy⟩, hy ▸ smul_mem_smul hyi (subset_span $ set.mem_singleton m)⟩
 
 theorem smul_le_right : I • N ≤ N :=
@@ -212,7 +212,7 @@ begin
   intros i,
   rw [← quotient.eq, ring_hom.map_sum],
   refine eq.trans (finset.sum_eq_single i _ _) _,
-  { intros j _ hji, rw quotient.eq_zero_iff_mem, exact (f i).mul_mem_left (hφ2 j i hji) },
+  { intros j _ hji, rw quotient.eq_zero_iff_mem, exact (f i).mul_mem_left _ (hφ2 j i hji) },
   { intros hi, exact (hi $ finset.mem_univ i).elim },
   specialize hφ1 i, rw [← quotient.eq, ring_hom.map_one] at hφ1,
   rw [ring_hom.map_mul, hφ1, mul_one]
@@ -266,10 +266,10 @@ theorem mul_le : I * J ≤ K ↔ ∀ (r ∈ I) (s ∈ J), r * s ∈ K :=
 submodule.smul_le
 
 lemma mul_le_left : I * J ≤ J :=
-ideal.mul_le.2 (λ r hr s, ideal.mul_mem_left _)
+ideal.mul_le.2 (λ r hr s, J.mul_mem_left _)
 
 lemma mul_le_right : I * J ≤ I :=
-ideal.mul_le.2 (λ r hr s hs, ideal.mul_mem_right _ hr)
+ideal.mul_le.2 (λ r hr s hs, I.mul_mem_right _ hr)
 
 @[simp] lemma sup_mul_right_self : I ⊔ (I * J) = I :=
 sup_eq_left.2 ideal.mul_le_right
@@ -303,7 +303,7 @@ lemma span_singleton_mul_span_singleton (r s : R) : span {r} * span {s} = (span
 by { unfold span, rw [submodule.span_mul_span, set.singleton_mul_singleton],}
 
 theorem mul_le_inf : I * J ≤ I ⊓ J :=
-mul_le.2 $ λ r hri s hsj, ⟨I.mul_mem_right hri, J.mul_mem_left hsj⟩
+mul_le.2 $ λ r hri s hsj, ⟨I.mul_mem_right s hri, J.mul_mem_left r hsj⟩
 
 theorem prod_le_inf {s : finset ι} {f : ι → ideal R} : s.prod f ≤ s.inf f :=
 begin
@@ -373,12 +373,12 @@ def radical (I : ideal R) : ideal R :=
     (add_pow x y (m + n)).symm ▸ I.sum_mem $
     show ∀ c ∈ finset.range (nat.succ (m + n)), x ^ c * y ^ (m + n - c) * (nat.choose (m + n) c) ∈ I,
     from λ c hc, or.cases_on (le_total c m)
-      (λ hcm, I.mul_mem_right $ I.mul_mem_left $ nat.add_comm n m ▸ (nat.add_sub_assoc hcm n).symm ▸
-        (pow_add y n (m-c)).symm ▸ I.mul_mem_right hyni)
-      (λ hmc, I.mul_mem_right $ I.mul_mem_right $ nat.add_sub_cancel' hmc ▸
-        (pow_add x m (c-m)).symm ▸ I.mul_mem_right hxmi)⟩,
-  smul_mem' := λ r s ⟨n, hsni⟩, ⟨n, show (r * s)^n ∈ I,
-    from (mul_pow r s n).symm ▸ I.mul_mem_left hsni⟩ }
+      (λ hcm, I.mul_mem_right _ $ I.mul_mem_left _ $ nat.add_comm n m ▸
+        (nat.add_sub_assoc hcm n).symm ▸
+        (pow_add y n (m-c)).symm ▸ I.mul_mem_right _ hyni)
+      (λ hmc, I.mul_mem_right _ $ I.mul_mem_right _ $ nat.add_sub_cancel' hmc ▸
+        (pow_add x m (c-m)).symm ▸ I.mul_mem_right _ hxmi)⟩,
+  smul_mem' := λ r s ⟨n, hsni⟩, ⟨n, (mul_pow r s n).symm ▸ I.mul_mem_left (r^n) hsni⟩ }
 
 theorem le_radical : I ≤ radical I :=
 λ r hri, ⟨1, (pow_one r).symm ▸ hri⟩
@@ -412,8 +412,8 @@ le_antisymm (radical_mono $ sup_le_sup le_radical le_radical) $
 
 theorem radical_inf : radical (I ⊓ J) = radical I ⊓ radical J :=
 le_antisymm (le_inf (radical_mono inf_le_left) (radical_mono inf_le_right))
-(λ r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩, ⟨m + n, (pow_add r m n).symm ▸ I.mul_mem_right hrm,
-(pow_add r m n).symm ▸ J.mul_mem_left hrn⟩)
+(λ r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩, ⟨m + n, (pow_add r m n).symm ▸ I.mul_mem_right _ hrm,
+(pow_add r m n).symm ▸ J.mul_mem_left _ hrn⟩)
 
 theorem radical_mul : radical (I * J) = radical I ⊓ radical J :=
 le_antisymm (radical_inf I J ▸ radical_mono $ @mul_le_inf _ _ I J)
@@ -439,7 +439,7 @@ have is_prime m, from ⟨by rintro rfl; rw radical_top at hrm; exact hrm trivial
   let ⟨n, hrn⟩ := this _ hxm, ⟨p, hpm, q, hq, hpqrn⟩ := submodule.mem_sup.1 hrn, ⟨c, hcxq⟩ := mem_span_singleton'.1 hq in
   let ⟨k, hrk⟩ := this _ hym, ⟨f, hfm, g, hg, hfgrk⟩ := submodule.mem_sup.1 hrk, ⟨d, hdyg⟩ := mem_span_singleton'.1 hg in
   hrm ⟨n + k, by rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c*x), mul_assoc c x (d*y), mul_left_comm x, ← mul_assoc];
-    refine m.add_mem (m.mul_mem_right hpm) (m.add_mem (m.mul_mem_left hfm) (m.mul_mem_left hxym))⟩⟩,
+    refine m.add_mem (m.mul_mem_right _ hpm) (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))⟩⟩,
 hrm $ this.radical.symm ▸ (Inf_le ⟨him, this⟩ : Inf {J : ideal R | I ≤ J ∧ is_prime J} ≤ m) hr
 
 @[simp] lemma radical_bot_of_integral_domain {R : Type u} [integral_domain R] :
@@ -675,7 +675,7 @@ span (f '' I)
 /-- `I.comap f` is the preimage of `I` under `f`. -/
 def comap (I : ideal S) : ideal R :=
 { carrier := f ⁻¹' I,
-  smul_mem' := λ c x hx, show f (c * x) ∈ I, by { rw f.map_mul, exact I.mul_mem_left hx },
+  smul_mem' := λ c x hx, show f (c * x) ∈ I, by { rw f.map_mul, exact I.mul_mem_left _ hx },
   .. I.to_add_submonoid.comap (f : R →+ S) }
 
 variables {f}

src/ring_theory/ideal/over.lean

@@ -39,7 +39,7 @@ lemma coeff_zero_mem_comap_of_root_mem_of_eval_mem {r : S} (hr : r ∈ I) {p : p
 begin
   rw [←p.div_X_mul_X_add, eval₂_add, eval₂_C, eval₂_mul, eval₂_X] at hp,
   refine mem_comap.mpr ((I.add_mem_iff_right _).mp hp),
-  exact I.mul_mem_left hr
+  exact I.mul_mem_left _ hr
 end
 
 lemma coeff_zero_mem_comap_of_root_mem {r : S} (hr : r ∈ I) {p : polynomial R}

src/ring_theory/ideal/prod.lean

@@ -26,14 +26,12 @@ def prod : ideal (R × S) :=
   add_mem' :=
   begin
     rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨ha₁, ha₂⟩ ⟨hb₁, hb₂⟩,
-    refine ⟨ideal.add_mem _ _ _, ideal.add_mem _ _ _⟩;
-    simp only [ha₁, ha₂, hb₁, hb₂]
+    exact ⟨I.add_mem ha₁ hb₁, J.add_mem ha₂ hb₂⟩
   end,
   smul_mem' :=
   begin
     rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨hb₁, hb₂⟩,
-    refine ⟨ideal.mul_mem_left _ _, ideal.mul_mem_left _ _⟩;
-    simp only [hb₁, hb₂]
+    exact ⟨I.mul_mem_left _ hb₁, J.mul_mem_left _ hb₂⟩,
   end }
 
 @[simp] lemma mem_prod {r : R} {s : S} : (⟨r, s⟩ : R × S) ∈ prod I J ↔ r ∈ I ∧ s ∈ J := iff.rfl
@@ -50,9 +48,7 @@ begin
     mem_map_iff_of_surjective (ring_hom.snd R S) prod.snd_surjective],
   refine ⟨λ h, ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, _⟩,
   rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩,
-  have hr : (r, s') * (1, 0) ∈ I := ideal.mul_mem_right _ h₁,
-  have hs : (r', s) * (0, 1) ∈ I := ideal.mul_mem_right _ h₂,
-  simpa using ideal.add_mem _ hr hs
+  simpa using I.add_mem (I.mul_mem_right (1, 0) h₁) (I.mul_mem_right (0, 1) h₂)
 end
 
 @[simp] lemma map_fst_prod (I : ideal R) (J : ideal S) : map (ring_hom.fst R S) (prod I J) = I :=

src/ring_theory/jacobson_ideal.lean

@@ -90,12 +90,12 @@ theorem mem_jacobson_iff {I : ideal R} {x : R} :
     suffices x ∉ M, from (this $ mem_Inf.1 hx ⟨le_trans le_sup_left hm2, hm1⟩).elim,
     λ hxm, hm1.1 $ (eq_top_iff_one _).2 $ add_sub_cancel' (x * y) 1 ▸ M.sub_mem
       (le_trans le_sup_right hm2 $ mem_span_singleton.2 $ dvd_refl _)
-      (M.mul_mem_right hxm)),
+      (M.mul_mem_right _ hxm)),
 λ hx, mem_Inf.2 $ λ M ⟨him, hm⟩, classical.by_contradiction $ λ hxm,
   let ⟨y, hy⟩ := hm.exists_inv hxm, ⟨z, hz⟩ := hx (-y) in
   hm.1 $ (eq_top_iff_one _).2 $ sub_sub_cancel (x * -y * z + z) 1 ▸ M.sub_mem
     (by rw [← one_mul z, ← mul_assoc, ← add_mul, mul_one, mul_neg_eq_neg_mul_symm, neg_add_eq_sub, ← neg_sub,
-        neg_mul_eq_neg_mul_symm, neg_mul_eq_mul_neg, mul_comm x y]; exact M.mul_mem_right hy)
+        neg_mul_eq_neg_mul_symm, neg_mul_eq_mul_neg, mul_comm x y]; exact M.mul_mem_right _ hy)
     (him hz)⟩
 
 /-- An ideal equals its Jacobson radical iff it is the intersection of a set of maximal ideals.
@@ -299,7 +299,7 @@ from le_antisymm (le_Inf $ λ M ⟨him, hm⟩, hm.is_prime.radical_le_iff.2 him)
 ⟨ne_top_of_lt $ lt_of_le_of_lt le_radical (lt_top_iff_ne_top.2 hi.1),
 λ x y hxy, ((is_local_of_is_maximal_radical hi).mem_jacobson_or_exists_inv y).symm.imp
   (λ ⟨z, hz⟩, by rw [← mul_one x, ← sub_sub_cancel (z * y) 1, mul_sub, mul_left_comm]; exact
-    I.sub_mem (I.mul_mem_left hxy) (I.mul_mem_left hz))
+    I.sub_mem (I.mul_mem_left _ hxy) (I.mul_mem_left _ hz))
   (this ▸ id)⟩
 
 

src/ring_theory/localization.lean

@@ -767,7 +767,8 @@ local_of_nonunits_ideal
     rw sub_eq_add_neg at hr,
     have := I.neg_mem_iff.1 ((ideal.add_mem_iff_right _ _).1 hr),
     { exact not_or (mt hp.mem_or_mem (not_or sx.2 sy.2)) sz.2 (hp.mem_or_mem this)},
-    { exact I.mul_mem_right (I.add_mem (I.mul_mem_right (this hx)) (I.mul_mem_right (this hy)))}
+    { exact I.mul_mem_right _ (I.add_mem (I.mul_mem_right _ (this hx))
+                                         (I.mul_mem_right _ (this hy)))}
   end)
 
 end localization_map
@@ -827,8 +828,8 @@ le_antisymm (ideal.map_le_iff_le_comap.2 (le_refl _)) $ λ x hJ,
 begin
   obtain ⟨r, s, hx⟩ := f.mk'_surjective x,
   rw ←hx at ⊢ hJ,
-  exact ideal.mul_mem_right _ (ideal.mem_map_of_mem (show f.to_map r ∈ J, from
-    f.mk'_spec r s ▸ @ideal.mul_mem_right _ _ J (f.mk' r s) (f.to_map s) hJ)),
+  exact ideal.mul_mem_right _ _ (ideal.mem_map_of_mem (show f.to_map r ∈ J, from
+    f.mk'_spec r s ▸ J.mul_mem_right (f.to_map s) hJ)),
 end
 
 theorem comap_map_of_is_prime_disjoint (I : ideal R) (hI : I.is_prime)

src/ring_theory/polynomial/basic.lean

@@ -222,7 +222,7 @@ open polynomial
 /-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself -/
 lemma polynomial_mem_ideal_of_coeff_mem_ideal (I : ideal (polynomial R)) (p : polynomial R)
   (hp : ∀ (n : ℕ), (p.coeff n) ∈ I.comap C) : p ∈ I :=
-sum_C_mul_X_eq p ▸ submodule.sum_mem I (λ n hn, I.mul_mem_right (hp n))
+sum_C_mul_X_eq p ▸ submodule.sum_mem I (λ n hn, I.mul_mem_right _ (hp n))
 
 /-- The push-forward of an ideal `I` of `R` to `polynomial R` via inclusion
  is exactly the set of polynomials whose coefficients are in `I` -/
@@ -394,7 +394,7 @@ begin
   { rintro ⟨p, hpI, hpdeg, rfl⟩,
     have : nat_degree p + (n - nat_degree p) = n,
     { exact nat.add_sub_cancel' (nat_degree_le_of_degree_le hpdeg) },
-    refine ⟨p * X ^ (n - nat_degree p), ⟨_, I.mul_mem_right hpI⟩, _⟩,
+    refine ⟨p * X ^ (n - nat_degree p), ⟨_, I.mul_mem_right _ hpI⟩, _⟩,
     { apply le_trans (degree_mul_le _ _) _,
       apply le_trans (add_le_add (degree_le_nat_degree) (degree_X_pow_le _)) _,
       rw [← with_bot.coe_add, this],
@@ -416,7 +416,7 @@ begin
   intros r hr,
   simp only [submodule.mem_coe, mem_leading_coeff_nth] at hr ⊢,
   rcases hr with ⟨p, hpI, hpdeg, rfl⟩,
-  refine ⟨p * X ^ (n - m), I.mul_mem_right hpI, _, leading_coeff_mul_X_pow⟩,
+  refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, _, leading_coeff_mul_X_pow⟩,
   refine le_trans (degree_mul_le _ _) _,
   refine le_trans (add_le_add hpdeg (degree_X_pow_le _)) _,
   rw [← with_bot.coe_add, nat.add_sub_cancel' H],
@@ -496,7 +496,7 @@ have hm2 : ∀ k, I.leading_coeff_nth k ≤ M := λ k, or.cases_on (le_or_lt k N
     this ⟨HN ▸ I.leading_coeff_nth_mono (le_of_lt h), λ H, hxm (H hx)⟩),
 have hs2 : ∀ {x}, x ∈ I.degree_le N → x ∈ ideal.span (↑s : set (polynomial R)),
 from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx) (ideal.zero_mem _)
-  (λ _ _, ideal.add_mem _) (λ c f hf, f.C_mul' c ▸ ideal.mul_mem_left _ hf),
+  (λ _ _, ideal.add_mem _) (λ c f hf, f.C_mul' c ▸ ideal.mul_mem_left _ _ hf),
 ⟨s, le_antisymm (ideal.span_le.2 $ λ x hx, have x ∈ I.degree_le N, from hs ▸ submodule.subset_span hx, this.2) $ begin
   change I ≤ ideal.span ↑s,
   intros p hp, generalize hn : p.nat_degree = k,
@@ -530,10 +530,10 @@ from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx)
     have := polynomial.degree_sub_lt h1 hp0 h2,
     rw [polynomial.degree_eq_nat_degree hp0] at this,
     rw ← sub_add_cancel p (q * polynomial.X ^ (k - q.nat_degree)),
-    refine (ideal.span ↑s).add_mem _ ((ideal.span ↑s).mul_mem_right _),
+    refine (ideal.span ↑s).add_mem _ ((ideal.span ↑s).mul_mem_right _ _),
     { by_cases hpq : p - q * polynomial.X ^ (k - q.nat_degree) = 0,
       { rw hpq, exact ideal.zero_mem _ },
-      refine ih _ _ (I.sub_mem hp (I.mul_mem_right hq)) rfl,
+      refine ih _ _ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl,
       rwa [polynomial.degree_eq_nat_degree hpq, with_bot.coe_lt_coe, hn] at this },
     exact hs2 ⟨polynomial.mem_degree_le.2 hdq, hq⟩ }
 end⟩⟩