bump to nightly-2023-09-16-06

mathlib commit leanprover-community/mathlib@001ffdc

Mathbin/Algebra/CovariantAndContravariant.lean

@@ -365,21 +365,17 @@ theorem covariant_lt_iff_contravariant_le [LinearOrder N] :
 #align covariant_lt_iff_contravariant_le covariant_lt_iff_contravariant_le
 -/
 
-#print covariant_flip_mul_iff /-
 @[to_additive]
-theorem covariant_flip_mul_iff [CommSemigroup N] :
+theorem covariant_flip_hMul_iff [CommSemigroup N] :
     Covariant N N (flip (· * ·)) r ↔ Covariant N N (· * ·) r := by rw [IsSymmOp.flip_eq]
-#align covariant_flip_mul_iff covariant_flip_mul_iff
+#align covariant_flip_mul_iff covariant_flip_hMul_iff
 #align covariant_flip_add_iff covariant_flip_add_iff
--/
 
-#print contravariant_flip_mul_iff /-
 @[to_additive]
-theorem contravariant_flip_mul_iff [CommSemigroup N] :
+theorem contravariant_flip_hMul_iff [CommSemigroup N] :
     Contravariant N N (flip (· * ·)) r ↔ Contravariant N N (· * ·) r := by rw [IsSymmOp.flip_eq]
-#align contravariant_flip_mul_iff contravariant_flip_mul_iff
+#align contravariant_flip_mul_iff contravariant_flip_hMul_iff
 #align contravariant_flip_add_iff contravariant_flip_add_iff
--/
 
 @[to_additive]
 instance contravariant_hMul_lt_of_covariant_hMul_le [Mul N] [LinearOrder N]
@@ -398,28 +394,28 @@ instance covariant_hMul_lt_of_contravariant_hMul_le [Mul N] [LinearOrder N]
 @[to_additive]
 instance covariant_swap_hMul_le_of_covariant_hMul_le [CommSemigroup N] [LE N]
     [CovariantClass N N (· * ·) (· ≤ ·)] : CovariantClass N N (swap (· * ·)) (· ≤ ·)
-    where elim := (covariant_flip_mul_iff N (· ≤ ·)).mpr CovariantClass.elim
+    where elim := (covariant_flip_hMul_iff N (· ≤ ·)).mpr CovariantClass.elim
 #align covariant_swap_mul_le_of_covariant_mul_le covariant_swap_hMul_le_of_covariant_hMul_le
 #align covariant_swap_add_le_of_covariant_add_le covariant_swap_add_le_of_covariant_add_le
 
 @[to_additive]
 instance contravariant_swap_hMul_le_of_contravariant_hMul_le [CommSemigroup N] [LE N]
     [ContravariantClass N N (· * ·) (· ≤ ·)] : ContravariantClass N N (swap (· * ·)) (· ≤ ·)
-    where elim := (contravariant_flip_mul_iff N (· ≤ ·)).mpr ContravariantClass.elim
+    where elim := (contravariant_flip_hMul_iff N (· ≤ ·)).mpr ContravariantClass.elim
 #align contravariant_swap_mul_le_of_contravariant_mul_le contravariant_swap_hMul_le_of_contravariant_hMul_le
 #align contravariant_swap_add_le_of_contravariant_add_le contravariant_swap_add_le_of_contravariant_add_le
 
 @[to_additive]
 instance contravariant_swap_hMul_lt_of_contravariant_hMul_lt [CommSemigroup N] [LT N]
     [ContravariantClass N N (· * ·) (· < ·)] : ContravariantClass N N (swap (· * ·)) (· < ·)
-    where elim := (contravariant_flip_mul_iff N (· < ·)).mpr ContravariantClass.elim
+    where elim := (contravariant_flip_hMul_iff N (· < ·)).mpr ContravariantClass.elim
 #align contravariant_swap_mul_lt_of_contravariant_mul_lt contravariant_swap_hMul_lt_of_contravariant_hMul_lt
 #align contravariant_swap_add_lt_of_contravariant_add_lt contravariant_swap_add_lt_of_contravariant_add_lt
 
 @[to_additive]
 instance covariant_swap_hMul_lt_of_covariant_hMul_lt [CommSemigroup N] [LT N]
     [CovariantClass N N (· * ·) (· < ·)] : CovariantClass N N (swap (· * ·)) (· < ·)
-    where elim := (covariant_flip_mul_iff N (· < ·)).mpr CovariantClass.elim
+    where elim := (covariant_flip_hMul_iff N (· < ·)).mpr CovariantClass.elim
 #align covariant_swap_mul_lt_of_covariant_mul_lt covariant_swap_hMul_lt_of_covariant_hMul_lt
 #align covariant_swap_add_lt_of_covariant_add_lt covariant_swap_add_lt_of_covariant_add_lt
 

Mathbin/Algebra/Group/UniqueProds.lean

@@ -220,9 +220,8 @@ instance {M} [Mul M] [UniqueProds M] : UniqueSums (Additive M)
 
 end Additive
 
-#print eq_and_eq_of_le_of_le_of_mul_le /-
 @[to_additive]
-theorem eq_and_eq_of_le_of_le_of_mul_le {A} [Mul A] [LinearOrder A]
+theorem eq_and_eq_of_le_of_le_of_hMul_le {A} [Mul A] [LinearOrder A]
     [CovariantClass A A (· * ·) (· ≤ ·)] [CovariantClass A A (Function.swap (· * ·)) (· < ·)]
     [ContravariantClass A A (· * ·) (· ≤ ·)] {a b a0 b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b)
     (ab : a * b ≤ a0 * b0) : a = a0 ∧ b = b0 :=
@@ -232,11 +231,9 @@ theorem eq_and_eq_of_le_of_le_of_mul_le {A} [Mul A] [LinearOrder A]
   have hb' : ¬a0 * b0 < a * b → ¬b0 < b := mt fun h => mul_lt_mul_of_le_of_lt ha h
   push_neg at ha' hb' 
   exact ⟨ha.antisymm' (ha' ab), hb.antisymm' (hb' ab)⟩
-#align eq_and_eq_of_le_of_le_of_mul_le eq_and_eq_of_le_of_le_of_mul_le
+#align eq_and_eq_of_le_of_le_of_mul_le eq_and_eq_of_le_of_le_of_hMul_le
 #align eq_and_eq_of_le_of_le_of_add_le eq_and_eq_of_le_of_le_of_add_le
--/
 
-#print Covariants.to_uniqueProds /-
 -- see Note [lower instance priority]
 /-- This instance asserts that if `A` has a multiplication, a linear order, and multiplication
 is 'very monotone', then `A` also has `unique_prods`. -/
@@ -247,8 +244,7 @@ instance (priority := 100) Covariants.to_uniqueProds {A} [Mul A] [LinearOrder A]
     [ContravariantClass A A (· * ·) (· ≤ ·)] : UniqueProds A
     where uniqueMul_of_nonempty A B hA hB :=
     ⟨_, A.min'_mem ‹_›, _, B.min'_mem ‹_›, fun a b ha hb ab =>
-      eq_and_eq_of_le_of_le_of_mul_le (Finset.min'_le _ _ ‹_›) (Finset.min'_le _ _ ‹_›) ab.le⟩
+      eq_and_eq_of_le_of_le_of_hMul_le (Finset.min'_le _ _ ‹_›) (Finset.min'_le _ _ ‹_›) ab.le⟩
 #align covariants.to_unique_prods Covariants.to_uniqueProds
-#align covariants.to_unique_sums Covariants.to_uniqueSums
--/
+#align covariants.to_unique_sums Covariants.to_unique_sums
 

Mathbin/Algebra/GroupPower/Order.lean

@@ -326,16 +326,14 @@ theorem lt_of_pow_lt_pow' {a b : M} (n : ℕ) : a ^ n < b ^ n → a < b :=
 #align lt_of_nsmul_lt_nsmul lt_of_nsmul_lt_nsmul
 -/
 
-#print min_lt_max_of_mul_lt_mul /-
 @[to_additive]
 theorem min_lt_max_of_mul_lt_mul {a b c d : M} (h : a * b < c * d) : min a b < max c d :=
   lt_of_pow_lt_pow' 2 <| by simp_rw [pow_two];
     exact
       (mul_le_mul' inf_le_left inf_le_right).trans_lt
         (h.trans_le <| mul_le_mul' le_sup_left le_sup_right)
-#align min_lt_max_of_mul_lt_mul min_lt_max_of_mul_lt_mul
-#align min_lt_max_of_add_lt_add min_lt_max_of_add_lt_add
--/
+#align min_lt_max_of_mul_lt_mul min_lt_max_of_mul_lt_mulₓ
+#align min_lt_max_of_add_lt_add min_lt_max_of_add_lt_addₓ
 
 #print min_lt_of_mul_lt_sq /-
 @[to_additive min_lt_of_add_lt_two_nsmul]

Mathbin/Algebra/MonoidAlgebra/NoZeroDivisors.lean

@@ -51,10 +51,9 @@ open Finsupp
 
 variable {R A : Type _} [Semiring R]
 
-#print AddMonoidAlgebra.mul_apply_add_eq_mul_of_forall_ne /-
 /-- The coefficient of a monomial in a product `f * g` that can be reached in at most one way
 as a product of monomials in the supports of `f` and `g` is a product. -/
-theorem mul_apply_add_eq_mul_of_forall_ne [Add A] {f g : AddMonoidAlgebra R A} {a0 b0 : A}
+theorem hMul_apply_add_eq_hMul_of_forall_ne [Add A] {f g : AddMonoidAlgebra R A} {a0 b0 : A}
     (h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0) :
     (f * g) (a0 + b0) = f a0 * g b0 := by
   classical
@@ -67,30 +66,24 @@ theorem mul_apply_add_eq_mul_of_forall_ne [Add A] {f g : AddMonoidAlgebra R A} {
       · exact if_neg (h af bg (Or.inr b0))
       · simp only [not_mem_support_iff.mp af, MulZeroClass.zero_mul, if_t_t]
     · exact fun bf0 => by simp [not_mem_support_iff.mp bf0]
-#align add_monoid_algebra.mul_apply_add_eq_mul_of_forall_ne AddMonoidAlgebra.mul_apply_add_eq_mul_of_forall_ne
--/
+#align add_monoid_algebra.mul_apply_add_eq_mul_of_forall_ne AddMonoidAlgebra.hMul_apply_add_eq_hMul_of_forall_ne
 
 section LeftOrRightOrderability
 
-#print AddMonoidAlgebra.Left.exists_add_of_mem_support_single_mul /-
-theorem Left.exists_add_of_mem_support_single_mul [AddLeftCancelSemigroup A]
+theorem Left.exists_add_of_mem_support_single_hMul [AddLeftCancelSemigroup A]
     {g : AddMonoidAlgebra R A} (a x : A)
     (hx : x ∈ (single a 1 * g : AddMonoidAlgebra R A).support) : ∃ b ∈ g.support, a + b = x := by
   rwa [support_single_mul _ _ (fun y => by rw [one_mul] : ∀ y : R, 1 * y = 0 ↔ _),
     Finset.mem_map] at hx 
-#align add_monoid_algebra.left.exists_add_of_mem_support_single_mul AddMonoidAlgebra.Left.exists_add_of_mem_support_single_mul
--/
+#align add_monoid_algebra.left.exists_add_of_mem_support_single_mul AddMonoidAlgebra.Left.exists_add_of_mem_support_single_hMul
 
-#print AddMonoidAlgebra.Right.exists_add_of_mem_support_single_mul /-
-theorem Right.exists_add_of_mem_support_single_mul [AddRightCancelSemigroup A]
+theorem Right.exists_add_of_mem_support_single_hMul [AddRightCancelSemigroup A]
     {f : AddMonoidAlgebra R A} (b x : A)
     (hx : x ∈ (f * single b 1 : AddMonoidAlgebra R A).support) : ∃ a ∈ f.support, a + b = x := by
   rwa [support_mul_single _ _ (fun y => by rw [mul_one] : ∀ y : R, y * 1 = 0 ↔ _),
     Finset.mem_map] at hx 
-#align add_monoid_algebra.right.exists_add_of_mem_support_single_mul AddMonoidAlgebra.Right.exists_add_of_mem_support_single_mul
--/
+#align add_monoid_algebra.right.exists_add_of_mem_support_single_mul AddMonoidAlgebra.Right.exists_add_of_mem_support_single_hMul
 
-#print AddMonoidAlgebra.NoZeroDivisors.of_left_ordered /-
 /-- If `R` is a semiring with no non-trivial zero-divisors and `A` is a left-ordered add right
 cancel semigroup, then `add_monoid_algebra R A` also contains no non-zero zero-divisors. -/
 theorem NoZeroDivisors.of_left_ordered [NoZeroDivisors R] [AddRightCancelSemigroup A]
@@ -128,9 +121,7 @@ theorem NoZeroDivisors.of_left_ordered [NoZeroDivisors R] [AddRightCancelSemigro
         · refine' add_lt_add_left _ _
           exact Finset.min'_lt_of_mem_erase_min' _ _ (finset.mem_erase.mpr ⟨hc, cg⟩)⟩
 #align add_monoid_algebra.no_zero_divisors.of_left_ordered AddMonoidAlgebra.NoZeroDivisors.of_left_ordered
--/
 
-#print AddMonoidAlgebra.NoZeroDivisors.of_right_ordered /-
 /-- If `R` is a semiring with no non-trivial zero-divisors and `A` is a right-ordered add left
 cancel semigroup, then `add_monoid_algebra R A` also contains no non-zero zero-divisors. -/
 theorem NoZeroDivisors.of_right_ordered [NoZeroDivisors R] [AddLeftCancelSemigroup A]
@@ -170,7 +161,6 @@ theorem NoZeroDivisors.of_right_ordered [NoZeroDivisors R] [AddLeftCancelSemigro
             Add.to_covariantClass_right A
           exact add_le_add_right (Finset.min'_le _ _ bf) _⟩
 #align add_monoid_algebra.no_zero_divisors.of_right_ordered AddMonoidAlgebra.NoZeroDivisors.of_right_ordered
--/
 
 end LeftOrRightOrderability
 

Mathbin/Algebra/Order/Monoid/Defs.lean

@@ -69,7 +69,6 @@ instance OrderedCommMonoid.to_covariantClass_right (M : Type _) [OrderedCommMono
 #align ordered_add_comm_monoid.to_covariant_class_right OrderedAddCommMonoid.to_covariantClass_right
 -/
 
-#print Mul.to_covariantClass_left /-
 /- This is not an instance, to avoid creating a loop in the type-class system: in a
 `left_cancel_semigroup` with a `partial_order`, assuming `covariant_class M M (*) (≤)` implies
 `covariant_class M M (*) (<)`, see `left_cancel_semigroup.covariant_mul_lt_of_covariant_mul_le`. -/
@@ -79,9 +78,7 @@ theorem Mul.to_covariantClass_left (M : Type _) [Mul M] [PartialOrder M]
   ⟨covariant_le_of_covariant_lt _ _ _ CovariantClass.elim⟩
 #align has_mul.to_covariant_class_left Mul.to_covariantClass_left
 #align has_add.to_covariant_class_left Add.to_covariantClass_left
--/
 
-#print Mul.to_covariantClass_right /-
 /- This is not an instance, to avoid creating a loop in the type-class system: in a
 `right_cancel_semigroup` with a `partial_order`, assuming `covariant_class M M (swap (*)) (<)`
 implies `covariant_class M M (swap (*)) (≤)`, see
@@ -92,7 +89,6 @@ theorem Mul.to_covariantClass_right (M : Type _) [Mul M] [PartialOrder M]
   ⟨covariant_le_of_covariant_lt _ _ _ CovariantClass.elim⟩
 #align has_mul.to_covariant_class_right Mul.to_covariantClass_right
 #align has_add.to_covariant_class_right Add.to_covariantClass_right
--/
 
 end OrderedInstances
 

Mathbin/Algebra/Order/Monoid/Lemmas.lean

@@ -1263,7 +1263,6 @@ theorem mul_eq_one_iff' [CovariantClass α α (· * ·) (· ≤ ·)]
 #align add_eq_zero_iff' add_eq_zero_iff'
 -/
 
-#print mul_le_mul_iff_of_ge /-
 @[to_additive]
 theorem mul_le_mul_iff_of_ge [CovariantClass α α (· * ·) (· ≤ ·)]
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] [CovariantClass α α (· * ·) (· < ·)]
@@ -1275,9 +1274,8 @@ theorem mul_le_mul_iff_of_ge [CovariantClass α α (· * ·) (· ≤ ·)]
   refine' ⟨fun ha => h.not_lt _, fun hb => h.not_lt _⟩
   · exact mul_lt_mul_of_lt_of_le ha hb
   · exact mul_lt_mul_of_le_of_lt ha hb
-#align mul_le_mul_iff_of_ge mul_le_mul_iff_of_ge
-#align add_le_add_iff_of_ge add_le_add_iff_of_ge
--/
+#align mul_le_mul_iff_of_ge mul_le_mul_iff_of_geₓ
+#align add_le_add_iff_of_ge add_le_add_iff_of_geₓ
 
 section Left
 
@@ -1383,9 +1381,8 @@ def Contravariant.toRightCancelSemigroup [ContravariantClass α α (swap (· * 
 #align contravariant.to_right_cancel_add_semigroup Contravariant.toAddRightCancelSemigroup
 -/
 
-#print Left.mul_eq_mul_iff_eq_and_eq /-
 @[to_additive]
-theorem Left.mul_eq_mul_iff_eq_and_eq [CovariantClass α α (· * ·) (· < ·)]
+theorem Left.hMul_eq_hMul_iff_eq_and_eq [CovariantClass α α (· * ·) (· < ·)]
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] [ContravariantClass α α (· * ·) (· ≤ ·)]
     [ContravariantClass α α (swap (· * ·)) (· ≤ ·)] {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) :
     a * b = c * d ↔ a = c ∧ b = d :=
@@ -1396,13 +1393,11 @@ theorem Left.mul_eq_mul_iff_eq_and_eq [CovariantClass α α (· * ·) (· < ·)]
   rcases eq_or_lt_of_le hbd with (rfl | hbd)
   · exact ⟨mul_right_cancel'' h, rfl⟩
   exact ((Left.mul_lt_mul hac hbd).Ne h).elim
-#align left.mul_eq_mul_iff_eq_and_eq Left.mul_eq_mul_iff_eq_and_eq
+#align left.mul_eq_mul_iff_eq_and_eq Left.hMul_eq_hMul_iff_eq_and_eq
 #align left.add_eq_add_iff_eq_and_eq Left.add_eq_add_iff_eq_and_eq
--/
 
-#print Right.mul_eq_mul_iff_eq_and_eq /-
 @[to_additive]
-theorem Right.mul_eq_mul_iff_eq_and_eq [CovariantClass α α (· * ·) (· ≤ ·)]
+theorem Right.hMul_eq_hMul_iff_eq_and_eq [CovariantClass α α (· * ·) (· ≤ ·)]
     [ContravariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· < ·)]
     [ContravariantClass α α (swap (· * ·)) (· ≤ ·)] {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) :
     a * b = c * d ↔ a = c ∧ b = d :=
@@ -1413,12 +1408,11 @@ theorem Right.mul_eq_mul_iff_eq_and_eq [CovariantClass α α (· * ·) (· ≤ 
   rcases eq_or_lt_of_le hbd with (rfl | hbd)
   · exact ⟨mul_right_cancel'' h, rfl⟩
   exact ((Right.mul_lt_mul hac hbd).Ne h).elim
-#align right.mul_eq_mul_iff_eq_and_eq Right.mul_eq_mul_iff_eq_and_eq
+#align right.mul_eq_mul_iff_eq_and_eq Right.hMul_eq_hMul_iff_eq_and_eq
 #align right.add_eq_add_iff_eq_and_eq Right.add_eq_add_iff_eq_and_eq
--/
 
-alias mul_eq_mul_iff_eq_and_eq := Left.mul_eq_mul_iff_eq_and_eq
-#align mul_eq_mul_iff_eq_and_eq mul_eq_mul_iff_eq_and_eq
+alias mul_eq_mul_iff_eq_and_eq := Left.hMul_eq_hMul_iff_eq_and_eq
+#align mul_eq_mul_iff_eq_and_eq mul_eq_mul_iff_eq_and_eqₓ
 
 attribute [to_additive] mul_eq_mul_iff_eq_and_eq
 
@@ -1813,23 +1807,19 @@ protected theorem inj [Mul α] [PartialOrder α] {a b c : α} (ha : MulLECancell
 #align add_le_cancellable.inj AddLECancellable.inj
 -/
 
-#print MulLECancellable.injective_left /-
 @[to_additive]
 protected theorem injective_left [CommSemigroup α] [PartialOrder α] {a : α}
     (ha : MulLECancellable a) : Injective (· * a) := fun b c h =>
   ha.Injective <| by rwa [mul_comm a, mul_comm a]
-#align mul_le_cancellable.injective_left MulLECancellable.injective_left
-#align add_le_cancellable.injective_left AddLECancellable.injective_left
--/
+#align mul_le_cancellable.injective_left MulLECancellable.injective_leftₓ
+#align add_le_cancellable.injective_left AddLECancellable.injective_leftₓ
 
-#print MulLECancellable.inj_left /-
 @[to_additive]
 protected theorem inj_left [CommSemigroup α] [PartialOrder α] {a b c : α}
     (hc : MulLECancellable c) : a * c = b * c ↔ a = b :=
-  hc.injective_left.eq_iff
-#align mul_le_cancellable.inj_left MulLECancellable.inj_left
-#align add_le_cancellable.inj_left AddLECancellable.inj_left
--/
+  hc.injective_leftₓ.eq_iff
+#align mul_le_cancellable.inj_left MulLECancellable.inj_leftₓ
+#align add_le_cancellable.inj_left AddLECancellable.inj_leftₓ
 
 variable [LE α]
 
@@ -1842,14 +1832,12 @@ protected theorem mul_le_mul_iff_left [Mul α] [CovariantClass α α (· * ·) (
 #align add_le_cancellable.add_le_add_iff_left AddLECancellable.add_le_add_iff_left
 -/
 
-#print MulLECancellable.mul_le_mul_iff_right /-
 @[to_additive]
 protected theorem mul_le_mul_iff_right [CommSemigroup α] [CovariantClass α α (· * ·) (· ≤ ·)]
     {a b c : α} (ha : MulLECancellable a) : b * a ≤ c * a ↔ b ≤ c := by
   rw [mul_comm b, mul_comm c, ha.mul_le_mul_iff_left]
-#align mul_le_cancellable.mul_le_mul_iff_right MulLECancellable.mul_le_mul_iff_right
-#align add_le_cancellable.add_le_add_iff_right AddLECancellable.add_le_add_iff_right
--/
+#align mul_le_cancellable.mul_le_mul_iff_right MulLECancellable.mul_le_mul_iff_rightₓ
+#align add_le_cancellable.add_le_add_iff_right AddLECancellable.add_le_add_iff_rightₓ
 
 #print MulLECancellable.le_mul_iff_one_le_right /-
 @[to_additive]
@@ -1869,23 +1857,19 @@ protected theorem mul_le_iff_le_one_right [MulOneClass α] [CovariantClass α α
 #align add_le_cancellable.add_le_iff_nonpos_right AddLECancellable.add_le_iff_nonpos_right
 -/
 
-#print MulLECancellable.le_mul_iff_one_le_left /-
 @[to_additive]
 protected theorem le_mul_iff_one_le_left [CommMonoid α] [CovariantClass α α (· * ·) (· ≤ ·)]
     {a b : α} (ha : MulLECancellable a) : a ≤ b * a ↔ 1 ≤ b := by
   rw [mul_comm, ha.le_mul_iff_one_le_right]
-#align mul_le_cancellable.le_mul_iff_one_le_left MulLECancellable.le_mul_iff_one_le_left
-#align add_le_cancellable.le_add_iff_nonneg_left AddLECancellable.le_add_iff_nonneg_left
--/
+#align mul_le_cancellable.le_mul_iff_one_le_left MulLECancellable.le_mul_iff_one_le_leftₓ
+#align add_le_cancellable.le_add_iff_nonneg_left AddLECancellable.le_add_iff_nonneg_leftₓ
 
-#print MulLECancellable.mul_le_iff_le_one_left /-
 @[to_additive]
 protected theorem mul_le_iff_le_one_left [CommMonoid α] [CovariantClass α α (· * ·) (· ≤ ·)]
     {a b : α} (ha : MulLECancellable a) : b * a ≤ a ↔ b ≤ 1 := by
   rw [mul_comm, ha.mul_le_iff_le_one_right]
-#align mul_le_cancellable.mul_le_iff_le_one_left MulLECancellable.mul_le_iff_le_one_left
-#align add_le_cancellable.add_le_iff_nonpos_left AddLECancellable.add_le_iff_nonpos_left
--/
+#align mul_le_cancellable.mul_le_iff_le_one_left MulLECancellable.mul_le_iff_le_one_leftₓ
+#align add_le_cancellable.add_le_iff_nonpos_left AddLECancellable.add_le_iff_nonpos_leftₓ
 
 end MulLECancellable
 

Mathbin/Algebra/Star/Order.lean

@@ -93,7 +93,7 @@ and obviates the hassle of `add_submonoid.closure_induction` when creating those
 If you are working with a `non_unital_ring` and not a `non_unital_semiring`, see
 `star_ordered_ring.of_nonneg_iff` for a more convenient version. -/
 @[reducible]
-def ofLeIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
+def ofLEIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
     (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
     (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R :=
   { ‹StarRing R› with
@@ -112,7 +112,7 @@ def ofLeIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
         · rintro a b ha hb x y rfl
           nth_rw 1 [← add_zero x]
           refine' h_add ((ha 0 _ (zero_add a).symm).trans (hb a _ rfl)) x }
-#align star_ordered_ring.of_le_iff StarOrderedRing.ofLeIffₓ
+#align star_ordered_ring.of_le_iff StarOrderedRing.ofLEIffₓ
 
 #print StarOrderedRing.ofNonnegIff /-
 -- set note [reducible non-instances]
@@ -146,7 +146,7 @@ instances. -/
 def ofNonnegIff' [NonUnitalRing R] [PartialOrder R] [StarRing R]
     (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
     (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) : StarOrderedRing R :=
-  ofLeIff (@h_add)
+  ofLEIff (@h_add)
     (by
       haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
       simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x))