fix counterexamples

astrainfinita · astrainfinita · commit 048b12044d9b · 2023-08-03T15:43:32.000+08:00
diff --git a/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean b/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean
@@ -11,16 +11,16 @@ import Mathlib.Algebra.Order.Monoid.Basic
 
 /-!
 
-A `CanonicallyOrderedCommSemiring` with two different elements `a` and `b` such that
+A canonically ordered commutative semiring with two different elements `a` and `b` such that
 `a ≠ b` and `2 * a = 2 * b`.  Thus, multiplication by a fixed non-zero element of a canonically
 ordered semiring need not be injective.  In particular, multiplying by a strictly positive element
 need not be strictly monotone.
 
-Recall that a `CanonicallyOrderedCommSemiring` is a commutative semiring with a partial ordering
-that is "canonical" in the sense that the inequality `a ≤ b` holds if and only if there is a `c`
-such that `a + c = b`.  There are several compatibility conditions among addition/multiplication
-and the order relation.  The point of the counterexample is to show that monotonicity of
-multiplication cannot be strengthened to **strict** monotonicity.
+Recall that a canonically ordered commutative semiring is a commutative semiring with a partial
+ordering that is "canonical" in the sense that the inequality `a ≤ b` holds if and only if there is
+a `c` such that `a + c = b`.  There are several compatibility conditions among
+addition/multiplication and the order relation.  The point of the counterexample is to show that
+monotonicity of multiplication cannot be strengthened to **strict** monotonicity.
 
 Reference:
 https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology
@@ -255,14 +255,15 @@ theorem eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : L, a * b = 0 → a = 0 ∨
     · exact (hb rfl).elim
 #align counterexample.ex_L.eq_zero_or_eq_zero_of_mul_eq_zero Counterexample.ExL.eq_zero_or_eq_zero_of_mul_eq_zero
 
-instance can : CanonicallyOrderedCommSemiring L :=
-  { (inferInstance : OrderBot L),
-    (inferInstance :
-      OrderedCommSemiring L) with
-    exists_add_of_le := @(exists_add_of_le)
-    le_self_add := le_self_add
-    eq_zero_or_eq_zero_of_mul_eq_zero := @(eq_zero_or_eq_zero_of_mul_eq_zero) }
-#align counterexample.ex_L.can Counterexample.ExL.can
+instance : OrderedCommSemiring L := inferInstance
+
+instance : CanonicallyOrderedAdd L where
+  exists_add_of_le := @(exists_add_of_le)
+  le_self_add := le_self_add
+  le_add_self a b := by rw [add_comm]; exact le_self_add _ _
+
+instance : NoZeroDivisors L where
+  eq_zero_or_eq_zero_of_mul_eq_zero := @(eq_zero_or_eq_zero_of_mul_eq_zero)
 
 /-- The elements `(1,0)` and `(1,1)` of `L` are different, but their doubles coincide.
 -/
