chore: rename mul_le_mul_right' to mul_le_mul_left (leanprover-community#30242)

Author: YaelDillies

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -349,7 +349,7 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
     intro i' hi' i'_i h2i'; constructor
     · apply le_trans h2i'.1
       simp [i, hw']
-    apply lt_of_lt_of_le (add_lt_add_left (mi_strict_minimal i'_i.symm hi') _)
+    apply lt_of_lt_of_le (add_lt_add_right (mi_strict_minimal i'_i.symm hi') _)
     simp [i, bi.symm, b_le_b hi']
   let s := bcubes cs c \ {i}
   have hs : s.Nonempty := by

Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean

@@ -16,6 +16,6 @@ The same applies to any superclasses, e.g. combining `StrictOrderedSemiring` wit
 
 example {α : Type*} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α]
     [BoundedOrder α] [Nontrivial α] : False :=
-  have top_pos := pos_of_lt_add_right (bot_le.trans_lt (add_lt_add_left bot_lt_top (⊥ : α)))
+  have top_pos := pos_of_lt_add_right (bot_le.trans_lt (add_lt_add_right bot_lt_top (⊥ : α)))
   have top_add_top_lt_self := lt_add_of_le_of_pos (@le_top _ _ _ (⊤ + ⊤)) top_pos
   top_add_top_lt_self.false

Mathlib/Algebra/Algebra/Operations.lean

@@ -819,7 +819,7 @@ theorem one_mem_div {I J : Submodule R A} : 1 ∈ I / J ↔ J ≤ I := by
   rw [← one_le, le_div_iff_mul_le, one_mul]
 
 theorem le_self_mul_one_div {I : Submodule R A} (hI : I ≤ 1) : I ≤ I * (1 / I) := by
-  simpa using mul_le_mul_left' (one_le_one_div.mpr hI) _
+  simpa using mul_le_mul_right (one_le_one_div.mpr hI) _
 
 theorem mul_one_div_le_one {I : Submodule R A} : I * (1 / I) ≤ 1 := by
   rw [Submodule.mul_le]

Mathlib/Algebra/Group/UniqueProds/Basic.lean

@@ -586,9 +586,9 @@ instance (priority := 100) of_covariant_right [IsRightCancelMul G]
     have : UniqueMul A B a0 b0 := by
       intro a b ha hb he
       obtain hl | rfl | hl := lt_trichotomy b b0
-      · exact ((he0 ▸ he ▸ mul_lt_mul_left' hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
+      · exact ((he0 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
       · exact ⟨mul_right_cancel he, rfl⟩
-      · exact ((he0 ▸ mul_lt_mul_left' hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim
+      · exact ((he0 ▸ mul_lt_mul_right hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim
     refine ⟨_, mk_mem_product ha0 hb0, _, mk_mem_product ha1 hb1, fun he ↦ ?_, this, ?_⟩
     · rw [Prod.mk_inj] at he; rw [he.1, he.2, he1] at he0
       obtain ⟨⟨a2, b2⟩, h2, hne⟩ := exists_mem_ne hc (a0, b0)
@@ -597,9 +597,9 @@ instance (priority := 100) of_covariant_right [IsRightCancelMul G]
       exact Prod.ext_iff.mpr (this h2.1 h2.2 he.symm)
     · intro a b ha hb he
       obtain hl | rfl | hl := lt_trichotomy b b1
-      · exact ((he1 ▸ mul_lt_mul_left' hl a1).not_ge <| min'_le _ _ <| mul_mem_mul ha1 hb).elim
+      · exact ((he1 ▸ mul_lt_mul_right hl a1).not_ge <| min'_le _ _ <| mul_mem_mul ha1 hb).elim
       · exact ⟨mul_right_cancel he, rfl⟩
-      · exact ((he1 ▸ he ▸ mul_lt_mul_left' hl a).not_ge <| min'_le _ _ <| mul_mem_mul ha hb1).elim
+      · exact ((he1 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| min'_le _ _ <| mul_mem_mul ha hb1).elim
 
 open MulOpposite in
 -- see Note [lower instance priority]
@@ -613,7 +613,7 @@ instance (priority := 100) of_covariant_left [IsLeftCancelMul G]
     TwoUniqueProds G :=
   let _ := LinearOrder.lift' (unop : Gᵐᵒᵖ → G) unop_injective
   let _ : MulLeftStrictMono Gᵐᵒᵖ :=
-    { elim := fun _ _ _ bc ↦ mul_lt_mul_right' (α := G) bc (unop _) }
+    { elim := fun _ _ _ bc ↦ mul_lt_mul_left (α := G) bc (unop _) }
   of_mulOpposite of_covariant_right
 
 end TwoUniqueProds

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -494,7 +494,7 @@ instance addCommMonoid : AddCommMonoid (LieSubalgebra R L) where
   nsmul := nsmulRec
 
 instance : IsOrderedAddMonoid (LieSubalgebra R L) where
-  add_le_add_left _ _ := sup_le_sup_left
+  add_le_add_left _ _ := sup_le_sup_right
 
 instance : CanonicallyOrderedAdd (LieSubalgebra R L) where
   exists_add_of_le {_a b} h := ⟨b, (sup_eq_right.2 h).symm⟩

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -168,8 +168,8 @@ theorem add_eq_sup (p q : Submodule R M) : p + q = p ⊔ q :=
 theorem zero_eq_bot : (0 : Submodule R M) = ⊥ :=
   rfl
 
-instance : IsOrderedAddMonoid (Submodule R M) :=
-  { add_le_add_left := fun _a _b => sup_le_sup_left }
+instance : IsOrderedAddMonoid (Submodule R M) where
+  add_le_add_left _ _ := sup_le_sup_right
 
 instance : CanonicallyOrderedAdd (Submodule R M) where
   exists_add_of_le {_a b} h := ⟨b, (sup_eq_right.2 h).symm⟩

Mathlib/Algebra/MonoidAlgebra/Degree.lean

@@ -314,7 +314,7 @@ theorem apply_add_of_supDegree_le (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2)
   rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
   · refine fun a ha hne => if_neg (fun he => ?_)
     apply_fun D at he; simp_rw [hadd] at he
-    exact (add_lt_add_left (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he
+    exact (add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he
   · intro h; rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
   · refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)
     apply_fun D at he

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -102,7 +102,7 @@ protected theorem add_le (x y : R) : abv (x + y) ≤ abv x + abv y :=
 lemma listSum_le [AddLeftMono S] (l : List R) : abv l.sum ≤ (l.map abv).sum := by
   induction l with
   | nil => simp
-  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_left ih (abv head)
+  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_right ih (abv head)
 
 @[simp]
 protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y :=

Mathlib/Algebra/Order/AddTorsor.lean

@@ -74,8 +74,8 @@ instance [LE G] [LE P] [SMul G P] [IsOrderedSMul G P] : CovariantClass G P (· 
 
 @[to_additive]
 instance [CommMonoid G] [PartialOrder G] [IsOrderedMonoid G] : IsOrderedSMul G G where
-  smul_le_smul_left _ _ := mul_le_mul_left'
-  smul_le_smul_right _ _ := mul_le_mul_right'
+  smul_le_smul_left _ _ := mul_le_mul_right
+  smul_le_smul_right _ _ := mul_le_mul_left
 
 @[to_additive]
 theorem IsOrderedSMul.smul_le_smul [LE G] [Preorder P] [SMul G P] [IsOrderedSMul G P]

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -265,7 +265,7 @@ theorem apply_prod_le_sum_map (h_one : f 1 ≤ 0) (h_mul : ∀ (a b : α), f (a
     f l.prod ≤ (l.map f).sum := by
   induction l with
   | nil => simp [h_one]
-  | cons hd tl IH => simpa using (h_mul _ _).trans (add_le_add_left IH _)
+  | cons hd tl IH => grw [prod_cons, h_mul, IH]; simp
 
 theorem sum_map_le_apply_prod (h_one : 0 ≤ f 1) (h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)) :
     (l.map f).sum ≤ f l.prod :=