diff --git a/Mathbin/Algebra/Order/LatticeGroup.lean b/Mathbin/Algebra/Order/LatticeGroup.lean
index e2e4b47c72..ffad35ed31 100644
--- a/Mathbin/Algebra/Order/LatticeGroup.lean
+++ b/Mathbin/Algebra/Order/LatticeGroup.lean
@@ -140,7 +140,7 @@ theorem inf_mul_sup [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : (a
 
 namespace LatticeOrderedCommGroup
 
-#print LatticeOrderedCommGroup.hasOneLatticeHasPosPart /-
+#print LatticeOrderedGroup.hasOneLatticeHasPosPart /-
 -- see Note [lower instance priority]
 /--
 Let `α` be a lattice ordered commutative group with identity `1`. For an element `a` of type `α`,
@@ -150,19 +150,19 @@ the element `a ⊔ 1` is said to be the *positive component* of `a`, denoted `a
       "\nLet `α` be a lattice ordered commutative group with identity `0`. For an element `a` of type `α`,\nthe element `a ⊔ 0` is said to be the *positive component* of `a`, denoted `a⁺`.\n"]
 instance (priority := 100) hasOneLatticeHasPosPart : PosPart α :=
   ⟨fun a => a ⊔ 1⟩
-#align lattice_ordered_comm_group.has_one_lattice_has_pos_part LatticeOrderedCommGroup.hasOneLatticeHasPosPart
-#align lattice_ordered_comm_group.has_zero_lattice_has_pos_part LatticeOrderedCommGroup.hasZeroLatticeHasPosPart
+#align lattice_ordered_comm_group.has_one_lattice_has_pos_part LatticeOrderedGroup.hasOneLatticeHasPosPart
+#align lattice_ordered_comm_group.has_zero_lattice_has_pos_part LatticeOrderedGroup.hasZeroLatticeHasPosPart
 -/
 
-#print LatticeOrderedCommGroup.m_pos_part_def /-
+#print LatticeOrderedGroup.m_pos_part_def /-
 @[to_additive pos_part_def]
 theorem m_pos_part_def (a : α) : a⁺ = a ⊔ 1 :=
   rfl
-#align lattice_ordered_comm_group.m_pos_part_def LatticeOrderedCommGroup.m_pos_part_def
-#align lattice_ordered_comm_group.pos_part_def LatticeOrderedCommGroup.pos_part_def
+#align lattice_ordered_comm_group.m_pos_part_def LatticeOrderedGroup.m_pos_part_def
+#align lattice_ordered_comm_group.pos_part_def LatticeOrderedGroup.pos_part_def
 -/
 
-#print LatticeOrderedCommGroup.hasOneLatticeHasNegPart /-
+#print LatticeOrderedGroup.hasOneLatticeHasNegPart /-
 -- see Note [lower instance priority]
 /--
 Let `α` be a lattice ordered commutative group with identity `1`. For an element `a` of type `α`,
@@ -172,155 +172,155 @@ the element `(-a) ⊔ 1` is said to be the *negative component* of `a`, denoted
       "\nLet `α` be a lattice ordered commutative group with identity `0`. For an element `a` of type `α`,\nthe element `(-a) ⊔ 0` is said to be the *negative component* of `a`, denoted `a⁻`.\n"]
 instance (priority := 100) hasOneLatticeHasNegPart : NegPart α :=
   ⟨fun a => a⁻¹ ⊔ 1⟩
-#align lattice_ordered_comm_group.has_one_lattice_has_neg_part LatticeOrderedCommGroup.hasOneLatticeHasNegPart
-#align lattice_ordered_comm_group.has_zero_lattice_has_neg_part LatticeOrderedCommGroup.hasZeroLatticeHasNegPart
+#align lattice_ordered_comm_group.has_one_lattice_has_neg_part LatticeOrderedGroup.hasOneLatticeHasNegPart
+#align lattice_ordered_comm_group.has_zero_lattice_has_neg_part LatticeOrderedGroup.hasZeroLatticeHasNegPart
 -/
 
-#print LatticeOrderedCommGroup.m_neg_part_def /-
+#print LatticeOrderedGroup.m_neg_part_def /-
 @[to_additive neg_part_def]
 theorem m_neg_part_def (a : α) : a⁻ = a⁻¹ ⊔ 1 :=
   rfl
-#align lattice_ordered_comm_group.m_neg_part_def LatticeOrderedCommGroup.m_neg_part_def
-#align lattice_ordered_comm_group.neg_part_def LatticeOrderedCommGroup.neg_part_def
+#align lattice_ordered_comm_group.m_neg_part_def LatticeOrderedGroup.m_neg_part_def
+#align lattice_ordered_comm_group.neg_part_def LatticeOrderedGroup.neg_part_def
 -/
 
-#print LatticeOrderedCommGroup.pos_one /-
+#print LatticeOrderedGroup.pos_one /-
 @[simp, to_additive]
 theorem pos_one : (1 : α)⁺ = 1 :=
   sup_idem
-#align lattice_ordered_comm_group.pos_one LatticeOrderedCommGroup.pos_one
-#align lattice_ordered_comm_group.pos_zero LatticeOrderedCommGroup.pos_zero
+#align lattice_ordered_comm_group.pos_one LatticeOrderedGroup.pos_one
+#align lattice_ordered_comm_group.pos_zero LatticeOrderedGroup.pos_zero
 -/
 
-#print LatticeOrderedCommGroup.neg_one /-
+#print LatticeOrderedGroup.neg_one /-
 @[simp, to_additive]
 theorem neg_one : (1 : α)⁻ = 1 := by rw [m_neg_part_def, inv_one, sup_idem]
-#align lattice_ordered_comm_group.neg_one LatticeOrderedCommGroup.neg_one
-#align lattice_ordered_comm_group.neg_zero LatticeOrderedCommGroup.neg_zero
+#align lattice_ordered_comm_group.neg_one LatticeOrderedGroup.neg_one
+#align lattice_ordered_comm_group.neg_zero LatticeOrderedGroup.neg_zero
 -/
 
-#print LatticeOrderedCommGroup.neg_eq_inv_inf_one /-
+#print LatticeOrderedGroup.neg_eq_inv_inf_one /-
 -- a⁻ = -(a ⊓ 0)
 @[to_additive]
 theorem neg_eq_inv_inf_one [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : a⁻ = (a ⊓ 1)⁻¹ := by
   rw [m_neg_part_def, ← inv_inj, inv_sup_eq_inv_inf_inv, inv_inv, inv_inv, inv_one]
-#align lattice_ordered_comm_group.neg_eq_inv_inf_one LatticeOrderedCommGroup.neg_eq_inv_inf_one
-#align lattice_ordered_comm_group.neg_eq_neg_inf_zero LatticeOrderedCommGroup.neg_eq_neg_inf_zero
+#align lattice_ordered_comm_group.neg_eq_inv_inf_one LatticeOrderedGroup.neg_eq_inv_inf_one
+#align lattice_ordered_comm_group.neg_eq_neg_inf_zero LatticeOrderedGroup.neg_eq_neg_inf_zero
 -/
 
-#print LatticeOrderedCommGroup.le_mabs /-
+#print LatticeOrderedGroup.le_mabs /-
 @[to_additive le_abs]
 theorem le_mabs (a : α) : a ≤ |a| :=
   le_sup_left
-#align lattice_ordered_comm_group.le_mabs LatticeOrderedCommGroup.le_mabs
-#align lattice_ordered_comm_group.le_abs LatticeOrderedCommGroup.le_abs
+#align lattice_ordered_comm_group.le_mabs LatticeOrderedGroup.le_mabs
+#align lattice_ordered_comm_group.le_abs LatticeOrderedGroup.le_abs
 -/
 
-#print LatticeOrderedCommGroup.inv_le_abs /-
+#print LatticeOrderedGroup.inv_le_abs /-
 -- -a ≤ |a|
 @[to_additive]
 theorem inv_le_abs (a : α) : a⁻¹ ≤ |a| :=
   le_sup_right
-#align lattice_ordered_comm_group.inv_le_abs LatticeOrderedCommGroup.inv_le_abs
-#align lattice_ordered_comm_group.neg_le_abs LatticeOrderedCommGroup.neg_le_abs
+#align lattice_ordered_comm_group.inv_le_abs LatticeOrderedGroup.inv_le_abs
+#align lattice_ordered_comm_group.neg_le_abs LatticeOrderedGroup.neg_le_abs
 -/
 
-#print LatticeOrderedCommGroup.one_le_pos /-
+#print LatticeOrderedGroup.one_le_pos /-
 -- 0 ≤ a⁺
 @[to_additive pos_nonneg]
 theorem one_le_pos (a : α) : 1 ≤ a⁺ :=
   le_sup_right
-#align lattice_ordered_comm_group.one_le_pos LatticeOrderedCommGroup.one_le_pos
-#align lattice_ordered_comm_group.pos_nonneg LatticeOrderedCommGroup.pos_nonneg
+#align lattice_ordered_comm_group.one_le_pos LatticeOrderedGroup.one_le_pos
+#align lattice_ordered_comm_group.pos_nonneg LatticeOrderedGroup.pos_nonneg
 -/
 
-#print LatticeOrderedCommGroup.one_le_neg /-
+#print LatticeOrderedGroup.one_le_neg /-
 -- 0 ≤ a⁻
 @[to_additive neg_nonneg]
 theorem one_le_neg (a : α) : 1 ≤ a⁻ :=
   le_sup_right
-#align lattice_ordered_comm_group.one_le_neg LatticeOrderedCommGroup.one_le_neg
-#align lattice_ordered_comm_group.neg_nonneg LatticeOrderedCommGroup.neg_nonneg
+#align lattice_ordered_comm_group.one_le_neg LatticeOrderedGroup.one_le_neg
+#align lattice_ordered_comm_group.neg_nonneg LatticeOrderedGroup.neg_nonneg
 -/
 
-#print LatticeOrderedCommGroup.pos_le_one_iff /-
+#print LatticeOrderedGroup.pos_le_one_iff /-
 -- pos_nonpos_iff
 @[to_additive]
 theorem pos_le_one_iff {a : α} : a⁺ ≤ 1 ↔ a ≤ 1 := by
   rw [m_pos_part_def, sup_le_iff, and_iff_left le_rfl]
-#align lattice_ordered_comm_group.pos_le_one_iff LatticeOrderedCommGroup.pos_le_one_iff
-#align lattice_ordered_comm_group.pos_nonpos_iff LatticeOrderedCommGroup.pos_nonpos_iff
+#align lattice_ordered_comm_group.pos_le_one_iff LatticeOrderedGroup.pos_le_one_iff
+#align lattice_ordered_comm_group.pos_nonpos_iff LatticeOrderedGroup.pos_nonpos_iff
 -/
 
-#print LatticeOrderedCommGroup.neg_le_one_iff /-
+#print LatticeOrderedGroup.neg_le_one_iff /-
 -- neg_nonpos_iff
 @[to_additive]
 theorem neg_le_one_iff {a : α} : a⁻ ≤ 1 ↔ a⁻¹ ≤ 1 := by
   rw [m_neg_part_def, sup_le_iff, and_iff_left le_rfl]
-#align lattice_ordered_comm_group.neg_le_one_iff LatticeOrderedCommGroup.neg_le_one_iff
-#align lattice_ordered_comm_group.neg_nonpos_iff LatticeOrderedCommGroup.neg_nonpos_iff
+#align lattice_ordered_comm_group.neg_le_one_iff LatticeOrderedGroup.neg_le_one_iff
+#align lattice_ordered_comm_group.neg_nonpos_iff LatticeOrderedGroup.neg_nonpos_iff
 -/
 
-#print LatticeOrderedCommGroup.pos_eq_one_iff /-
+#print LatticeOrderedGroup.pos_eq_one_iff /-
 @[to_additive]
 theorem pos_eq_one_iff {a : α} : a⁺ = 1 ↔ a ≤ 1 :=
   sup_eq_right
-#align lattice_ordered_comm_group.pos_eq_one_iff LatticeOrderedCommGroup.pos_eq_one_iff
-#align lattice_ordered_comm_group.pos_eq_zero_iff LatticeOrderedCommGroup.pos_eq_zero_iff
+#align lattice_ordered_comm_group.pos_eq_one_iff LatticeOrderedGroup.pos_eq_one_iff
+#align lattice_ordered_comm_group.pos_eq_zero_iff LatticeOrderedGroup.pos_eq_zero_iff
 -/
 
-#print LatticeOrderedCommGroup.neg_eq_one_iff' /-
+#print LatticeOrderedGroup.neg_eq_one_iff' /-
 @[to_additive]
 theorem neg_eq_one_iff' {a : α} : a⁻ = 1 ↔ a⁻¹ ≤ 1 :=
   sup_eq_right
-#align lattice_ordered_comm_group.neg_eq_one_iff' LatticeOrderedCommGroup.neg_eq_one_iff'
-#align lattice_ordered_comm_group.neg_eq_zero_iff' LatticeOrderedCommGroup.neg_eq_zero_iff'
+#align lattice_ordered_comm_group.neg_eq_one_iff' LatticeOrderedGroup.neg_eq_one_iff'
+#align lattice_ordered_comm_group.neg_eq_zero_iff' LatticeOrderedGroup.neg_eq_zero_iff'
 -/
 
-#print LatticeOrderedCommGroup.neg_eq_one_iff /-
+#print LatticeOrderedGroup.neg_eq_one_iff /-
 @[to_additive]
 theorem neg_eq_one_iff [CovariantClass α α Mul.mul LE.le] {a : α} : a⁻ = 1 ↔ 1 ≤ a := by
   rw [le_antisymm_iff, neg_le_one_iff, inv_le_one', and_iff_left (one_le_neg _)]
-#align lattice_ordered_comm_group.neg_eq_one_iff LatticeOrderedCommGroup.neg_eq_one_iff
-#align lattice_ordered_comm_group.neg_eq_zero_iff LatticeOrderedCommGroup.neg_eq_zero_iff
+#align lattice_ordered_comm_group.neg_eq_one_iff LatticeOrderedGroup.neg_eq_one_iff
+#align lattice_ordered_comm_group.neg_eq_zero_iff LatticeOrderedGroup.neg_eq_zero_iff
 -/
 
-#print LatticeOrderedCommGroup.m_le_pos /-
+#print LatticeOrderedGroup.m_le_pos /-
 @[to_additive le_pos]
 theorem m_le_pos (a : α) : a ≤ a⁺ :=
   le_sup_left
-#align lattice_ordered_comm_group.m_le_pos LatticeOrderedCommGroup.m_le_pos
-#align lattice_ordered_comm_group.le_pos LatticeOrderedCommGroup.le_pos
+#align lattice_ordered_comm_group.m_le_pos LatticeOrderedGroup.m_le_pos
+#align lattice_ordered_comm_group.le_pos LatticeOrderedGroup.le_pos
 -/
 
-#print LatticeOrderedCommGroup.inv_le_neg /-
+#print LatticeOrderedGroup.inv_le_neg /-
 -- -a ≤ a⁻
 @[to_additive]
 theorem inv_le_neg (a : α) : a⁻¹ ≤ a⁻ :=
   le_sup_left
-#align lattice_ordered_comm_group.inv_le_neg LatticeOrderedCommGroup.inv_le_neg
-#align lattice_ordered_comm_group.neg_le_neg LatticeOrderedCommGroup.neg_le_neg
+#align lattice_ordered_comm_group.inv_le_neg LatticeOrderedGroup.inv_le_neg
+#align lattice_ordered_comm_group.neg_le_neg LatticeOrderedGroup.neg_le_neg
 -/
 
-#print LatticeOrderedCommGroup.neg_eq_pos_inv /-
+#print LatticeOrderedGroup.neg_eq_pos_inv /-
 -- Bourbaki A.VI.12
 --  a⁻ = (-a)⁺
 @[to_additive]
 theorem neg_eq_pos_inv (a : α) : a⁻ = a⁻¹⁺ :=
   rfl
-#align lattice_ordered_comm_group.neg_eq_pos_inv LatticeOrderedCommGroup.neg_eq_pos_inv
-#align lattice_ordered_comm_group.neg_eq_pos_neg LatticeOrderedCommGroup.neg_eq_pos_neg
+#align lattice_ordered_comm_group.neg_eq_pos_inv LatticeOrderedGroup.neg_eq_pos_inv
+#align lattice_ordered_comm_group.neg_eq_pos_neg LatticeOrderedGroup.neg_eq_pos_neg
 -/
 
-#print LatticeOrderedCommGroup.pos_eq_neg_inv /-
+#print LatticeOrderedGroup.pos_eq_neg_inv /-
 -- a⁺ = (-a)⁻
 @[to_additive]
 theorem pos_eq_neg_inv (a : α) : a⁺ = a⁻¹⁻ := by rw [neg_eq_pos_inv, inv_inv]
-#align lattice_ordered_comm_group.pos_eq_neg_inv LatticeOrderedCommGroup.pos_eq_neg_inv
-#align lattice_ordered_comm_group.pos_eq_neg_neg LatticeOrderedCommGroup.pos_eq_neg_neg
+#align lattice_ordered_comm_group.pos_eq_neg_inv LatticeOrderedGroup.pos_eq_neg_inv
+#align lattice_ordered_comm_group.pos_eq_neg_neg LatticeOrderedGroup.pos_eq_neg_neg
 -/
 
-#print LatticeOrderedCommGroup.pos_div_neg /-
+#print LatticeOrderedGroup.pos_div_neg /-
 -- Bourbaki A.VI.12  Prop 9 a)
 -- a = a⁺ - a⁻
 @[simp, to_additive]
@@ -330,19 +330,19 @@ theorem pos_div_neg [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : a⁺
   rw [div_eq_mul_inv]
   apply eq_mul_inv_of_mul_eq
   rw [m_neg_part_def, mul_sup, mul_one, mul_right_inv, sup_comm, m_pos_part_def]
-#align lattice_ordered_comm_group.pos_div_neg LatticeOrderedCommGroup.pos_div_neg
-#align lattice_ordered_comm_group.pos_sub_neg LatticeOrderedCommGroup.pos_sub_neg
+#align lattice_ordered_comm_group.pos_div_neg LatticeOrderedGroup.pos_div_neg
+#align lattice_ordered_comm_group.pos_sub_neg LatticeOrderedGroup.pos_sub_neg
 -/
 
-#print LatticeOrderedCommGroup.pos_inf_neg_eq_one /-
+#print LatticeOrderedGroup.pos_inf_neg_eq_one /-
 -- Bourbaki A.VI.12  Prop 9 a)
 -- a⁺ ⊓ a⁻ = 0 (`a⁺` and `a⁻` are co-prime, and, since they are positive, disjoint)
 @[to_additive]
 theorem pos_inf_neg_eq_one [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : a⁺ ⊓ a⁻ = 1 := by
   rw [← mul_right_inj (a⁻)⁻¹, mul_inf, mul_one, mul_left_inv, mul_comm, ← div_eq_mul_inv,
     pos_div_neg, neg_eq_inv_inf_one, inv_inv]
-#align lattice_ordered_comm_group.pos_inf_neg_eq_one LatticeOrderedCommGroup.pos_inf_neg_eq_one
-#align lattice_ordered_comm_group.pos_inf_neg_eq_zero LatticeOrderedCommGroup.pos_inf_neg_eq_zero
+#align lattice_ordered_comm_group.pos_inf_neg_eq_one LatticeOrderedGroup.pos_inf_neg_eq_one
+#align lattice_ordered_comm_group.pos_inf_neg_eq_zero LatticeOrderedGroup.pos_inf_neg_eq_zero
 -/
 
 #print LatticeOrderedCommGroup.sup_eq_mul_pos_div /-
@@ -393,7 +393,7 @@ theorem m_le_iff_pos_le_neg_ge [CovariantClass α α (· * ·) (· ≤ ·)] (a b
 #align lattice_ordered_comm_group.le_iff_pos_le_neg_ge LatticeOrderedCommGroup.le_iff_pos_le_neg_ge
 -/
 
-#print LatticeOrderedCommGroup.m_neg_abs /-
+#print LatticeOrderedGroup.m_neg_abs /-
 @[to_additive neg_abs]
 theorem m_neg_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a|⁻ = 1 :=
   by
@@ -404,11 +404,11 @@ theorem m_neg_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a|⁻
       exact ((m_le_iff_pos_le_neg_ge _ _).mp (inv_le_abs a)).right
     · exact And.right (Iff.mp (m_le_iff_pos_le_neg_ge _ _) (le_mabs a))
   · exact one_le_neg _
-#align lattice_ordered_comm_group.m_neg_abs LatticeOrderedCommGroup.m_neg_abs
-#align lattice_ordered_comm_group.neg_abs LatticeOrderedCommGroup.neg_abs
+#align lattice_ordered_comm_group.m_neg_abs LatticeOrderedGroup.m_neg_abs
+#align lattice_ordered_comm_group.neg_abs LatticeOrderedGroup.neg_abs
 -/
 
-#print LatticeOrderedCommGroup.m_pos_abs /-
+#print LatticeOrderedGroup.m_pos_abs /-
 @[to_additive pos_abs]
 theorem m_pos_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a|⁺ = |a| :=
   by
@@ -417,19 +417,17 @@ theorem m_pos_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a|⁺
   symm
   rw [mul_right_eq_self, inv_eq_one]
   exact m_neg_abs a
-#align lattice_ordered_comm_group.m_pos_abs LatticeOrderedCommGroup.m_pos_abs
-#align lattice_ordered_comm_group.pos_abs LatticeOrderedCommGroup.pos_abs
+#align lattice_ordered_comm_group.m_pos_abs LatticeOrderedGroup.m_pos_abs
+#align lattice_ordered_comm_group.pos_abs LatticeOrderedGroup.pos_abs
 -/
 
-#print LatticeOrderedCommGroup.one_le_abs /-
 @[to_additive abs_nonneg]
 theorem one_le_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : 1 ≤ |a| := by rw [← m_pos_abs];
   exact one_le_pos _
 #align lattice_ordered_comm_group.one_le_abs LatticeOrderedCommGroup.one_le_abs
 #align lattice_ordered_comm_group.abs_nonneg LatticeOrderedCommGroup.abs_nonneg
--/
 
-#print LatticeOrderedCommGroup.pos_mul_neg /-
+#print LatticeOrderedGroup.pos_mul_neg /-
 -- |a| = a⁺ - a⁻
 @[to_additive]
 theorem pos_mul_neg [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a| = a⁺ * a⁻ :=
@@ -437,11 +435,11 @@ theorem pos_mul_neg [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a|
   rw [m_pos_part_def, sup_mul, one_mul, m_neg_part_def, mul_sup, mul_one, mul_inv_self, sup_assoc, ←
     @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]
   exact (sup_eq_left.2 <| one_le_abs a).symm
-#align lattice_ordered_comm_group.pos_mul_neg LatticeOrderedCommGroup.pos_mul_neg
-#align lattice_ordered_comm_group.pos_add_neg LatticeOrderedCommGroup.pos_add_neg
+#align lattice_ordered_comm_group.pos_mul_neg LatticeOrderedGroup.pos_mul_neg
+#align lattice_ordered_comm_group.pos_add_neg LatticeOrderedGroup.pos_add_neg
 -/
 
-#print LatticeOrderedCommGroup.sup_div_inf_eq_abs_div /-
+#print LatticeOrderedGroup.sup_div_inf_eq_abs_div /-
 -- a ⊔ b - (a ⊓ b) = |b - a|
 @[to_additive]
 theorem sup_div_inf_eq_abs_div [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) :
@@ -449,8 +447,8 @@ theorem sup_div_inf_eq_abs_div [CovariantClass α α (· * ·) (· ≤ ·)] (a b
   rw [sup_eq_mul_pos_div, inf_comm, inf_eq_div_pos_div, div_eq_mul_inv, div_eq_mul_inv b ((b / a)⁺),
     mul_inv_rev, inv_inv, mul_comm, ← mul_assoc, inv_mul_cancel_right, pos_eq_neg_inv (a / b),
     div_eq_mul_inv a b, mul_inv_rev, ← div_eq_mul_inv, inv_inv, ← pos_mul_neg]
-#align lattice_ordered_comm_group.sup_div_inf_eq_abs_div LatticeOrderedCommGroup.sup_div_inf_eq_abs_div
-#align lattice_ordered_comm_group.sup_sub_inf_eq_abs_sub LatticeOrderedCommGroup.sup_sub_inf_eq_abs_sub
+#align lattice_ordered_comm_group.sup_div_inf_eq_abs_div LatticeOrderedGroup.sup_div_inf_eq_abs_div
+#align lattice_ordered_comm_group.sup_sub_inf_eq_abs_sub LatticeOrderedGroup.sup_sub_inf_eq_abs_sub
 -/
 
 #print LatticeOrderedCommGroup.sup_sq_eq_mul_mul_abs_div /-
@@ -527,16 +525,16 @@ theorem abs_div_sup_mul_abs_div_inf [CovariantClass α α (· * ·) (· ≤ ·)]
 #align lattice_ordered_comm_group.abs_sub_sup_add_abs_sub_inf LatticeOrderedCommGroup.abs_sub_sup_add_abs_sub_inf
 -/
 
-#print LatticeOrderedCommGroup.pos_of_one_le /-
+#print LatticeOrderedGroup.pos_of_one_le /-
 -- pos_of_nonneg
 /-- If `a` is positive, then it is equal to its positive component `a⁺`. -/
 @[to_additive "If `a` is positive, then it is equal to its positive component `a⁺`."]
 theorem pos_of_one_le (a : α) (h : 1 ≤ a) : a⁺ = a := by rw [m_pos_part_def]; exact sup_of_le_left h
-#align lattice_ordered_comm_group.pos_of_one_le LatticeOrderedCommGroup.pos_of_one_le
-#align lattice_ordered_comm_group.pos_of_nonneg LatticeOrderedCommGroup.pos_of_nonneg
+#align lattice_ordered_comm_group.pos_of_one_le LatticeOrderedGroup.pos_of_one_le
+#align lattice_ordered_comm_group.pos_of_nonneg LatticeOrderedGroup.pos_of_nonneg
 -/
 
-#print LatticeOrderedCommGroup.pos_eq_self_of_one_lt_pos /-
+#print LatticeOrderedGroup.pos_eq_self_of_one_lt_pos /-
 -- pos_eq_self_of_pos_pos
 @[to_additive]
 theorem pos_eq_self_of_one_lt_pos {α} [LinearOrder α] [CommGroup α] {x : α} (hx : 1 < x⁺) :
@@ -544,71 +542,71 @@ theorem pos_eq_self_of_one_lt_pos {α} [LinearOrder α] [CommGroup α] {x : α}
   rw [m_pos_part_def, right_lt_sup, not_le] at hx 
   rw [m_pos_part_def, sup_eq_left]
   exact hx.le
-#align lattice_ordered_comm_group.pos_eq_self_of_one_lt_pos LatticeOrderedCommGroup.pos_eq_self_of_one_lt_pos
-#align lattice_ordered_comm_group.pos_eq_self_of_pos_pos LatticeOrderedCommGroup.pos_eq_self_of_pos_pos
+#align lattice_ordered_comm_group.pos_eq_self_of_one_lt_pos LatticeOrderedGroup.pos_eq_self_of_one_lt_pos
+#align lattice_ordered_comm_group.pos_eq_self_of_pos_pos LatticeOrderedGroup.pos_eq_self_of_pos_pos
 -/
 
-#print LatticeOrderedCommGroup.pos_of_le_one /-
+#print LatticeOrderedGroup.pos_of_le_one /-
 -- 0 ≤ a implies a⁺ = a
 -- pos_of_nonpos
 @[to_additive]
 theorem pos_of_le_one (a : α) (h : a ≤ 1) : a⁺ = 1 :=
   pos_eq_one_iff.mpr h
-#align lattice_ordered_comm_group.pos_of_le_one LatticeOrderedCommGroup.pos_of_le_one
-#align lattice_ordered_comm_group.pos_of_nonpos LatticeOrderedCommGroup.pos_of_nonpos
+#align lattice_ordered_comm_group.pos_of_le_one LatticeOrderedGroup.pos_of_le_one
+#align lattice_ordered_comm_group.pos_of_nonpos LatticeOrderedGroup.pos_of_nonpos
 -/
 
-#print LatticeOrderedCommGroup.neg_of_one_le_inv /-
+#print LatticeOrderedGroup.neg_of_one_le_inv /-
 @[to_additive neg_of_inv_nonneg]
 theorem neg_of_one_le_inv (a : α) (h : 1 ≤ a⁻¹) : a⁻ = a⁻¹ := by rw [neg_eq_pos_inv];
   exact pos_of_one_le _ h
-#align lattice_ordered_comm_group.neg_of_one_le_inv LatticeOrderedCommGroup.neg_of_one_le_inv
-#align lattice_ordered_comm_group.neg_of_inv_nonneg LatticeOrderedCommGroup.neg_of_inv_nonneg
+#align lattice_ordered_comm_group.neg_of_one_le_inv LatticeOrderedGroup.neg_of_one_le_inv
+#align lattice_ordered_comm_group.neg_of_inv_nonneg LatticeOrderedGroup.neg_of_inv_nonneg
 -/
 
-#print LatticeOrderedCommGroup.neg_of_inv_le_one /-
+#print LatticeOrderedGroup.neg_of_inv_le_one /-
 -- neg_of_neg_nonpos
 @[to_additive]
 theorem neg_of_inv_le_one (a : α) (h : a⁻¹ ≤ 1) : a⁻ = 1 :=
   neg_eq_one_iff'.mpr h
-#align lattice_ordered_comm_group.neg_of_inv_le_one LatticeOrderedCommGroup.neg_of_inv_le_one
-#align lattice_ordered_comm_group.neg_of_neg_nonpos LatticeOrderedCommGroup.neg_of_neg_nonpos
+#align lattice_ordered_comm_group.neg_of_inv_le_one LatticeOrderedGroup.neg_of_inv_le_one
+#align lattice_ordered_comm_group.neg_of_neg_nonpos LatticeOrderedGroup.neg_of_neg_nonpos
 -/
 
-#print LatticeOrderedCommGroup.neg_of_le_one /-
+#print LatticeOrderedGroup.neg_of_le_one /-
 -- neg_of_nonpos
 @[to_additive]
 theorem neg_of_le_one [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : a ≤ 1) : a⁻ = a⁻¹ :=
   sup_eq_left.2 <| one_le_inv'.2 h
-#align lattice_ordered_comm_group.neg_of_le_one LatticeOrderedCommGroup.neg_of_le_one
-#align lattice_ordered_comm_group.neg_of_nonpos LatticeOrderedCommGroup.neg_of_nonpos
+#align lattice_ordered_comm_group.neg_of_le_one LatticeOrderedGroup.neg_of_le_one
+#align lattice_ordered_comm_group.neg_of_nonpos LatticeOrderedGroup.neg_of_nonpos
 -/
 
-#print LatticeOrderedCommGroup.neg_of_one_le /-
+#print LatticeOrderedGroup.neg_of_one_le /-
 -- neg_of_nonneg'
 @[to_additive]
 theorem neg_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : 1 ≤ a) : a⁻ = 1 :=
   neg_eq_one_iff.mpr h
-#align lattice_ordered_comm_group.neg_of_one_le LatticeOrderedCommGroup.neg_of_one_le
-#align lattice_ordered_comm_group.neg_of_nonneg LatticeOrderedCommGroup.neg_of_nonneg
+#align lattice_ordered_comm_group.neg_of_one_le LatticeOrderedGroup.neg_of_one_le
+#align lattice_ordered_comm_group.neg_of_nonneg LatticeOrderedGroup.neg_of_nonneg
 -/
 
-#print LatticeOrderedCommGroup.mabs_of_one_le /-
+#print LatticeOrderedGroup.mabs_of_one_le /-
 -- 0 ≤ a implies |a| = a
 @[to_additive abs_of_nonneg]
 theorem mabs_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : 1 ≤ a) : |a| = a :=
   sup_eq_left.2 <| Left.inv_le_self h
-#align lattice_ordered_comm_group.mabs_of_one_le LatticeOrderedCommGroup.mabs_of_one_le
-#align lattice_ordered_comm_group.abs_of_nonneg LatticeOrderedCommGroup.abs_of_nonneg
+#align lattice_ordered_comm_group.mabs_of_one_le LatticeOrderedGroup.mabs_of_one_le
+#align lattice_ordered_comm_group.abs_of_nonneg LatticeOrderedGroup.abs_of_nonneg
 -/
 
-#print LatticeOrderedCommGroup.mabs_mabs /-
+#print LatticeOrderedGroup.mabs_mabs /-
 /-- The unary operation of taking the absolute value is idempotent. -/
 @[simp, to_additive abs_abs "The unary operation of taking the absolute value is idempotent."]
 theorem mabs_mabs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : ||a|| = |a| :=
   mabs_of_one_le _ (one_le_abs _)
-#align lattice_ordered_comm_group.mabs_mabs LatticeOrderedCommGroup.mabs_mabs
-#align lattice_ordered_comm_group.abs_abs LatticeOrderedCommGroup.abs_abs
+#align lattice_ordered_comm_group.mabs_mabs LatticeOrderedGroup.mabs_mabs
+#align lattice_ordered_comm_group.abs_abs LatticeOrderedGroup.abs_abs
 -/
 
 #print LatticeOrderedCommGroup.mabs_sup_div_sup_le_mabs /-
@@ -662,15 +660,15 @@ theorem mabs_mul_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : |a
 #align lattice_ordered_comm_group.abs_add_le LatticeOrderedCommGroup.abs_add_le
 -/
 
-#print LatticeOrderedCommGroup.abs_div_comm /-
+#print LatticeOrderedGroup.abs_div_comm /-
 -- |a - b| = |b - a|
 @[to_additive]
 theorem abs_div_comm (a b : α) : |a / b| = |b / a| :=
   by
   unfold Abs.abs
   rw [inv_div a b, ← inv_inv (a / b), inv_div, sup_comm]
-#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedCommGroup.abs_div_comm
-#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedCommGroup.abs_sub_comm
+#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedGroup.abs_div_comm
+#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedGroup.abs_sub_comm
 -/
 
 #print LatticeOrderedCommGroup.abs_abs_div_abs_le /-
diff --git a/Mathbin/Algebra/Quandle.lean b/Mathbin/Algebra/Quandle.lean
index 9541f6d8b2..d9de75f727 100644
--- a/Mathbin/Algebra/Quandle.lean
+++ b/Mathbin/Algebra/Quandle.lean
@@ -408,10 +408,12 @@ variable {S₁ : Type _} {S₂ : Type _} {S₃ : Type _} [Shelf S₁] [Shelf S
 instance : CoeFun (S₁ →◃ S₂) fun _ => S₁ → S₂ :=
   ⟨ShelfHom.toFun⟩
 
+#print ShelfHom.toFun_eq_coe /-
 @[simp]
 theorem toFun_eq_coe (f : S₁ →◃ S₂) : f.toFun = f :=
   rfl
 #align shelf_hom.to_fun_eq_coe ShelfHom.toFun_eq_coe
+-/
 
 #print ShelfHom.map_act /-
 @[simp]
diff --git a/Mathbin/Data/Complex/Basic.lean b/Mathbin/Data/Complex/Basic.lean
index 15c5daa93c..0575c38f95 100644
--- a/Mathbin/Data/Complex/Basic.lean
+++ b/Mathbin/Data/Complex/Basic.lean
@@ -1400,7 +1400,6 @@ theorem eq_re_ofReal_le {r : ℝ} {z : ℂ} (hz : (r : ℂ) ≤ z) : z = z.re :=
 #align complex.eq_re_of_real_le Complex.eq_re_ofReal_le
 -/
 
-#print Complex.strictOrderedCommRing /-
 /-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a strictly ordered ring.
 -/
 protected def strictOrderedCommRing : StrictOrderedCommRing ℂ :=
@@ -1411,11 +1410,9 @@ protected def strictOrderedCommRing : StrictOrderedCommRing ℂ :=
     mul_pos := fun z w hz hw => by
       simp [lt_def, mul_re, mul_im, ← hz.2, ← hw.2, mul_pos hz.1 hw.1] }
 #align complex.strict_ordered_comm_ring Complex.strictOrderedCommRing
--/
 
 scoped[ComplexOrder] attribute [instance] Complex.strictOrderedCommRing
 
-#print Complex.starOrderedRing /-
 /-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a star ordered ring.
 (That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)
 -/
@@ -1435,7 +1432,6 @@ protected def starOrderedRing : StarOrderedRing ℂ :=
     · obtain ⟨s, rfl⟩ := h
       simp only [← norm_sq_eq_conj_mul_self, norm_sq_nonneg, zero_le_real, star_def]
 #align complex.star_ordered_ring Complex.starOrderedRing
--/
 
 scoped[ComplexOrder] attribute [instance] Complex.starOrderedRing
 
diff --git a/Mathbin/Data/Complex/Module.lean b/Mathbin/Data/Complex/Module.lean
index adc043f0bb..72e78f1e2e 100644
--- a/Mathbin/Data/Complex/Module.lean
+++ b/Mathbin/Data/Complex/Module.lean
@@ -152,11 +152,9 @@ section
 
 open scoped ComplexOrder
 
-#print Complex.orderedSMul /-
 protected theorem orderedSMul : OrderedSMul ℝ ℂ :=
   OrderedSMul.mk' fun a b r hab hr => ⟨by simp [hr, hab.1.le], by simp [hab.2]⟩
 #align complex.ordered_smul Complex.orderedSMul
--/
 
 scoped[ComplexOrder] attribute [instance] Complex.orderedSMul
 
diff --git a/Mathbin/LinearAlgebra/Matrix/Diagonal.lean b/Mathbin/LinearAlgebra/Matrix/Diagonal.lean
index 4865441401..3631ad4779 100644
--- a/Mathbin/LinearAlgebra/Matrix/Diagonal.lean
+++ b/Mathbin/LinearAlgebra/Matrix/Diagonal.lean
@@ -94,7 +94,7 @@ theorem range_diagonal [DecidableEq m] (w : m → K) :
 #align matrix.range_diagonal Matrix.range_diagonal
 -/
 
-#print Matrix.rank_diagonal /-
+#print LinearMap.rank_diagonal /-
 theorem rank_diagonal [DecidableEq m] [DecidableEq K] (w : m → K) :
     rank (diagonal w).toLin' = Fintype.card { i // w i ≠ 0 } :=
   by
@@ -105,7 +105,7 @@ theorem rank_diagonal [DecidableEq m] [DecidableEq K] (w : m → K) :
   rw [rank, range_diagonal, B₁, ← @rank_fun' K]
   apply LinearEquiv.rank_eq
   apply B₂
-#align matrix.rank_diagonal Matrix.rank_diagonal
+#align matrix.rank_diagonal LinearMap.rank_diagonal
 -/
 
 end Field
diff --git a/Mathbin/Probability/Martingale/Convergence.lean b/Mathbin/Probability/Martingale/Convergence.lean
index 51f20fb640..965820f2d7 100644
--- a/Mathbin/Probability/Martingale/Convergence.lean
+++ b/Mathbin/Probability/Martingale/Convergence.lean
@@ -196,10 +196,8 @@ theorem Submartingale.upcrossings_ae_lt_top' [IsFiniteMeasure μ] (hf : Submarti
       refine' lintegral_mono fun ω => _
       rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm]
       by_cases hnonneg : 0 ≤ f n ω - a
-      ·
-        rw [LatticeOrderedCommGroup.pos_of_nonneg _ hnonneg, Real.norm_eq_abs,
-          abs_of_nonneg hnonneg]
-      · rw [LatticeOrderedCommGroup.pos_of_nonpos _ (not_le.1 hnonneg).le]
+      · rw [LatticeOrderedGroup.pos_of_nonneg _ hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
+      · rw [LatticeOrderedGroup.pos_of_nonpos _ (not_le.1 hnonneg).le]
         exact norm_nonneg _
       · simp only [Ne.def, ENNReal.coe_ne_top, not_false_iff]
     · simp only [hab, Ne.def, ENNReal.ofReal_eq_zero, sub_nonpos, not_le]
diff --git a/Mathbin/Probability/Martingale/Upcrossing.lean b/Mathbin/Probability/Martingale/Upcrossing.lean
index b1d48f6145..f300d63009 100644
--- a/Mathbin/Probability/Martingale/Upcrossing.lean
+++ b/Mathbin/Probability/Martingale/Upcrossing.lean
@@ -879,13 +879,13 @@ theorem crossing_pos_eq (hab : a < b) :
     refine' ⟨fun h => _, fun h => _⟩
     ·
       rwa [← sub_le_sub_iff_right a, ←
-        LatticeOrderedCommGroup.pos_eq_self_of_pos_pos (lt_of_lt_of_le hab' h)]
+        LatticeOrderedGroup.pos_eq_self_of_pos_pos (lt_of_lt_of_le hab' h)]
     · rw [← sub_le_sub_iff_right a] at h 
-      rwa [LatticeOrderedCommGroup.pos_of_nonneg _ (le_trans hab'.le h)]
+      rwa [LatticeOrderedGroup.pos_of_nonneg _ (le_trans hab'.le h)]
   have hf' : ∀ ω i, (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a :=
     by
     intro ω i
-    rw [LatticeOrderedCommGroup.pos_nonpos_iff, sub_nonpos]
+    rw [LatticeOrderedGroup.pos_nonpos_iff, sub_nonpos]
   induction' n with k ih
   · refine' ⟨rfl, _⟩
     simp only [lower_crossing_time_zero, hitting, Set.mem_Icc, Set.mem_Iic]
@@ -938,8 +938,8 @@ theorem mul_integral_upcrossingsBefore_le_integral_pos_part_aux [IsFiniteMeasure
   refine'
     le_trans (le_of_eq _)
       (integral_mul_upcrossings_before_le_integral (hf.sub_martingale (martingale_const _ _ _)).Pos
-        (fun ω => LatticeOrderedCommGroup.pos_nonneg _)
-        (fun ω => LatticeOrderedCommGroup.pos_nonneg _) (sub_pos.2 hab))
+        (fun ω => LatticeOrderedGroup.pos_nonneg _) (fun ω => LatticeOrderedGroup.pos_nonneg _)
+        (sub_pos.2 hab))
   simp_rw [sub_zero, ← upcrossings_before_pos_eq hab]
   rfl
 #align measure_theory.mul_integral_upcrossings_before_le_integral_pos_part_aux MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux
@@ -959,7 +959,7 @@ theorem Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part [IsFin
   · rw [not_lt, ← sub_nonpos] at hab 
     exact
       le_trans (mul_nonpos_of_nonpos_of_nonneg hab (integral_nonneg fun ω => Nat.cast_nonneg _))
-        (integral_nonneg fun ω => LatticeOrderedCommGroup.pos_nonneg _)
+        (integral_nonneg fun ω => LatticeOrderedGroup.pos_nonneg _)
 #align measure_theory.submartingale.mul_integral_upcrossings_before_le_integral_pos_part MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part
 -/
 
@@ -1110,7 +1110,7 @@ theorem Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part [IsFiniteM
       intro N
       rw [of_real_integral_eq_lintegral_of_real]
       · exact (hf.sub_martingale (martingale_const _ _ _)).Pos.Integrable _
-      · exact eventually_of_forall fun ω => LatticeOrderedCommGroup.pos_nonneg _
+      · exact eventually_of_forall fun ω => LatticeOrderedGroup.pos_nonneg _
     rw [lintegral_supr']
     · simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]
       intro N
diff --git a/Mathbin/Probability/StrongLaw.lean b/Mathbin/Probability/StrongLaw.lean
index c7f1b98729..ca5cd90001 100644
--- a/Mathbin/Probability/StrongLaw.lean
+++ b/Mathbin/Probability/StrongLaw.lean
@@ -637,7 +637,7 @@ theorem strong_law_aux2 {c : ℝ} (c_one : 1 < c) :
   apply Asymptotics.isLittleO_iff.2 fun ε εpos => _
   obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists
   filter_upwards [hω i] with n hn
-  simp only [Real.norm_eq_abs, LatticeOrderedCommGroup.abs_abs, Nat.abs_cast]
+  simp only [Real.norm_eq_abs, LatticeOrderedGroup.abs_abs, Nat.abs_cast]
   exact hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))
 #align probability_theory.strong_law_aux2 ProbabilityTheory.strong_law_aux2
 -/
diff --git a/lake-manifest.json b/lake-manifest.json
index 81d7a6683b..3f7a132620 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "0ebb88163badde5b820d016c0d0d54cc120dfcf3",
+    "rev": "99776ef2e96168a7c84fc705ee5f342b9165be7b",
     "name": "lean3port",
-    "inputRev?": "0ebb88163badde5b820d016c0d0d54cc120dfcf3"}},
+    "inputRev?": "99776ef2e96168a7c84fc705ee5f342b9165be7b"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "2d11c668314a5b2e55f34f7b65964118fcb1ff9f",
+    "rev": "f330b65348432a6e7dc2c49403394517886f8c32",
     "name": "mathlib",
-    "inputRev?": "2d11c668314a5b2e55f34f7b65964118fcb1ff9f"}},
+    "inputRev?": "f330b65348432a6e7dc2c49403394517886f8c32"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 058fcf3e8b..dfc4d36589 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-08-10-07"
+def tag : String := "nightly-2023-08-10-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"0ebb88163badde5b820d016c0d0d54cc120dfcf3"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"99776ef2e96168a7c84fc705ee5f342b9165be7b"
 
 @[default_target]
 lean_lib Mathbin where