oops

src/Init/Grind/Module/Basic.lean

@@ -20,6 +20,9 @@ class AddRightCancel (M : Type u) [Add M] where
   /-- Addition is right-cancellative. -/
   add_right_cancel : ∀ a b c : M, a + c = b + c → a = b
 
+/-- A type with zero and addition,
+where addition is commutative and associative,
+and the zero is the right identity for addition. -/
 class AddCommMonoid (M : Type u) extends Zero M, Add M where
   /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : M, a + 0 = a
@@ -30,6 +33,9 @@ class AddCommMonoid (M : Type u) extends Zero M, Add M where
 
 attribute [instance 100] AddCommMonoid.toZero AddCommMonoid.toAdd
 
+/-- A type with zero, addition, negation, and subtraction,
+where addition is commutative and associative,
+and negation is the left inverse of addition. -/
 class AddCommGroup (M : Type u) extends AddCommMonoid M, Neg M, Sub M where
   /-- Negation is the left inverse of addition. -/
   neg_add_cancel : ∀ a : M, -a + a = 0

src/Init/Grind/Ordered/Order.lean

@@ -18,7 +18,6 @@ class Preorder (α : Type u) [LE α] [LT α] where
   le_refl : ∀ a : α, a ≤ a
   /-- The less-than-or-equal relation is transitive. -/
   le_trans : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c
-  lt := fun a b : α => a ≤ b ∧ ¬b ≤ a
   /-- The less-than relation is determined by the less-than-or-equal relation. -/
   lt_iff_le_not_le : ∀ {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl