From 428acaae08005d2204bfd9abb24ecb0fdcbd9497 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Tue, 6 Dec 2022 04:12:22 +0000
Subject: [PATCH] move(algebra/order/monoid/*): relocate `zero_le_one_class`
 again (#17820)

#17646 move `zero_le_one_class` to `algebra.order.monoid.with_zero`. This PR split things about `zero_le_one_class` into two files.

Also, all lemmas about numerics other than 0 and 1 require typeclass `add_monoid_with_one` now.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/OfNat)
---
 src/algebra/order/monoid/nat_cast.lean       | 84 ++++++++++++++++++
 src/algebra/order/monoid/with_zero/defs.lean | 93 +-------------------
 src/algebra/order/ring/defs.lean             |  1 +
 src/algebra/order/zero_le_one.lean           | 42 +++++++++
 src/combinatorics/set_family/kleitman.lean   |  2 +-
 5 files changed, 129 insertions(+), 93 deletions(-)
 create mode 100644 src/algebra/order/monoid/nat_cast.lean
 create mode 100644 src/algebra/order/zero_le_one.lean

diff --git a/src/algebra/order/monoid/nat_cast.lean b/src/algebra/order/monoid/nat_cast.lean
new file mode 100644
index 0000000000000..d41fd0f420862
--- /dev/null
+++ b/src/algebra/order/monoid/nat_cast.lean
@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl, Yuyang Zhao
+-/
+import algebra.order.monoid.lemmas
+import algebra.order.zero_le_one
+import data.nat.cast.defs
+
+/-!
+# Order of numerials in an `add_monoid_with_one`.
+-/
+
+variable {α : Type*}
+
+open function
+
+lemma lt_add_one [has_one α] [add_zero_class α] [partial_order α] [zero_le_one_class α]
+  [ne_zero (1 : α)] [covariant_class α α (+) (<)] (a : α) : a < a + 1 :=
+lt_add_of_pos_right _ zero_lt_one
+
+lemma lt_one_add [has_one α] [add_zero_class α] [partial_order α] [zero_le_one_class α]
+  [ne_zero (1 : α)] [covariant_class α α (swap (+)) (<)] (a : α) : a < 1 + a :=
+lt_add_of_pos_left _ zero_lt_one
+
+variable [add_monoid_with_one α]
+
+lemma zero_le_two [preorder α] [zero_le_one_class α] [covariant_class α α (+) (≤)] :
+  (0 : α) ≤ 2 :=
+add_nonneg zero_le_one zero_le_one
+
+lemma zero_le_three [preorder α] [zero_le_one_class α] [covariant_class α α (+) (≤)] :
+  (0 : α) ≤ 3 :=
+add_nonneg zero_le_two zero_le_one
+
+lemma zero_le_four [preorder α] [zero_le_one_class α] [covariant_class α α (+) (≤)] :
+  (0 : α) ≤ 4 :=
+add_nonneg zero_le_two zero_le_two
+
+lemma one_le_two [has_le α] [zero_le_one_class α] [covariant_class α α (+) (≤)] :
+  (1 : α) ≤ 2 :=
+calc 1 = 1 + 0 : (add_zero 1).symm
+   ... ≤ 1 + 1 : add_le_add_left zero_le_one _
+
+lemma one_le_two' [has_le α] [zero_le_one_class α] [covariant_class α α (swap (+)) (≤)] :
+  (1 : α) ≤ 2 :=
+calc 1 = 0 + 1 : (zero_add 1).symm
+   ... ≤ 1 + 1 : add_le_add_right zero_le_one _
+
+section
+variables [partial_order α] [zero_le_one_class α] [ne_zero (1 : α)]
+
+section
+variables [covariant_class α α (+) (≤)]
+
+/-- See `zero_lt_two'` for a version with the type explicit. -/
+@[simp] lemma zero_lt_two : (0 : α) < 2 := zero_lt_one.trans_le one_le_two
+/-- See `zero_lt_three'` for a version with the type explicit. -/
+@[simp] lemma zero_lt_three : (0 : α) < 3 := lt_add_of_lt_of_nonneg zero_lt_two zero_le_one
+/-- See `zero_lt_four'` for a version with the type explicit. -/
+@[simp] lemma zero_lt_four : (0 : α) < 4 := lt_add_of_lt_of_nonneg zero_lt_two zero_le_two
+
+variables (α)
+
+/-- See `zero_lt_two` for a version with the type implicit. -/
+lemma zero_lt_two' : (0 : α) < 2 := zero_lt_two
+/-- See `zero_lt_three` for a version with the type implicit. -/
+lemma zero_lt_three' : (0 : α) < 3 := zero_lt_three
+/-- See `zero_lt_four` for a version with the type implicit. -/
+lemma zero_lt_four' : (0 : α) < 4 := zero_lt_four
+
+instance zero_le_one_class.ne_zero.two : ne_zero (2 : α) := ⟨zero_lt_two.ne'⟩
+instance zero_le_one_class.ne_zero.three : ne_zero (3 : α) := ⟨zero_lt_three.ne'⟩
+instance zero_le_one_class.ne_zero.four : ne_zero (4 : α) := ⟨zero_lt_four.ne'⟩
+
+end
+
+lemma one_lt_two [covariant_class α α (+) (<)] : (1 : α) < 2 := lt_add_one _
+
+end
+
+alias zero_lt_two ← two_pos
+alias zero_lt_three ← three_pos
+alias zero_lt_four ← four_pos
diff --git a/src/algebra/order/monoid/with_zero/defs.lean b/src/algebra/order/monoid/with_zero/defs.lean
index c0f6c4b9aa3b9..b7cf46e79022d 100644
--- a/src/algebra/order/monoid/with_zero/defs.lean
+++ b/src/algebra/order/monoid/with_zero/defs.lean
@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import algebra.group.with_one.defs
 import algebra.order.monoid.canonical.defs
+import algebra.order.zero_le_one
 
 /-!
 # Adjoining a zero element to an ordered monoid.
@@ -12,15 +13,9 @@ import algebra.order.monoid.canonical.defs
 
 set_option old_structure_cmd true
 
-open function
-
 universe u
 variables {α : Type u}
 
-/-- Typeclass for expressing that the `0` of a type is less or equal to its `1`. -/
-class zero_le_one_class (α : Type*) [has_zero α] [has_one α] [has_le α] :=
-(zero_le_one : (0 : α) ≤ 1)
-
 /-- A linearly ordered commutative monoid with a zero element. -/
 class linear_ordered_comm_monoid_with_zero (α : Type*)
   extends linear_ordered_comm_monoid α, comm_monoid_with_zero α :=
@@ -36,92 +31,6 @@ instance canonically_ordered_add_monoid.to_zero_le_one_class [canonically_ordere
   [has_one α] : zero_le_one_class α :=
 ⟨zero_le 1⟩
 
-/-- `zero_le_one` with the type argument implicit. -/
-@[simp] lemma zero_le_one [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
-zero_le_one_class.zero_le_one
-
-/-- `zero_le_one` with the type argument explicit. -/
-lemma zero_le_one' (α) [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
-zero_le_one
-
-lemma zero_le_two [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
-  [covariant_class α α (+) (≤)] : (0 : α) ≤ 2 :=
-add_nonneg zero_le_one zero_le_one
-
-lemma zero_le_three [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
-  [covariant_class α α (+) (≤)] : (0 : α) ≤ 3 :=
-add_nonneg zero_le_two zero_le_one
-
-lemma zero_le_four [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
-  [covariant_class α α (+) (≤)] : (0 : α) ≤ 4 :=
-add_nonneg zero_le_two zero_le_two
-
-lemma one_le_two [has_le α] [has_one α] [add_zero_class α] [zero_le_one_class α]
-  [covariant_class α α (+) (≤)] : (1 : α) ≤ 2 :=
-calc 1 = 1 + 0 : (add_zero 1).symm
-   ... ≤ 1 + 1 : add_le_add_left zero_le_one _
-
-lemma one_le_two' [has_le α] [has_one α] [add_zero_class α] [zero_le_one_class α]
-  [covariant_class α α (swap (+)) (≤)] : (1 : α) ≤ 2 :=
-calc 1 = 0 + 1 : (zero_add 1).symm
-   ... ≤ 1 + 1 : add_le_add_right zero_le_one _
-
-section
-variables [has_zero α] [has_one α] [partial_order α] [zero_le_one_class α] [ne_zero (1 : α)]
-
-/-- See `zero_lt_one'` for a version with the type explicit. -/
-@[simp] lemma zero_lt_one : (0 : α) < 1 := zero_le_one.lt_of_ne (ne_zero.ne' 1)
-
-variables (α)
-
-/-- See `zero_lt_one` for a version with the type implicit. -/
-lemma zero_lt_one' : (0 : α) < 1 := zero_lt_one
-
-end
-
-section
-variables [has_one α] [add_zero_class α] [partial_order α] [zero_le_one_class α] [ne_zero (1 : α)]
-
-section
-variables [covariant_class α α (+) (≤)]
-
-/-- See `zero_lt_two'` for a version with the type explicit. -/
-@[simp] lemma zero_lt_two : (0 : α) < 2 := zero_lt_one.trans_le one_le_two
-/-- See `zero_lt_three'` for a version with the type explicit. -/
-@[simp] lemma zero_lt_three : (0 : α) < 3 := lt_add_of_lt_of_nonneg zero_lt_two zero_le_one
-/-- See `zero_lt_four'` for a version with the type explicit. -/
-@[simp] lemma zero_lt_four : (0 : α) < 4 := lt_add_of_lt_of_nonneg zero_lt_two zero_le_two
-
-variables (α)
-
-/-- See `zero_lt_two` for a version with the type implicit. -/
-lemma zero_lt_two' : (0 : α) < 2 := zero_lt_two
-/-- See `zero_lt_three` for a version with the type implicit. -/
-lemma zero_lt_three' : (0 : α) < 3 := zero_lt_three
-/-- See `zero_lt_four` for a version with the type implicit. -/
-lemma zero_lt_four' : (0 : α) < 4 := zero_lt_four
-
-instance zero_le_one_class.ne_zero.two : ne_zero (2 : α) := ⟨zero_lt_two.ne'⟩
-instance zero_le_one_class.ne_zero.three : ne_zero (3 : α) := ⟨zero_lt_three.ne'⟩
-instance zero_le_one_class.ne_zero.four : ne_zero (4 : α) := ⟨zero_lt_four.ne'⟩
-
-end
-
-lemma lt_add_one [covariant_class α α (+) (<)] (a : α) : a < a + 1 :=
-lt_add_of_pos_right _ zero_lt_one
-
-lemma lt_one_add [covariant_class α α (swap (+)) (<)] (a : α) : a < 1 + a :=
-lt_add_of_pos_left _ zero_lt_one
-
-lemma one_lt_two [covariant_class α α (+) (<)] : (1 : α) < 2 := lt_add_one _
-
-end
-
-alias zero_lt_one ← one_pos
-alias zero_lt_two ← two_pos
-alias zero_lt_three ← three_pos
-alias zero_lt_four ← four_pos
-
 namespace with_zero
 
 local attribute [semireducible] with_zero
diff --git a/src/algebra/order/ring/defs.lean b/src/algebra/order/ring/defs.lean
index f6a5d815b25bd..612305ddff8a8 100644
--- a/src/algebra/order/ring/defs.lean
+++ b/src/algebra/order/ring/defs.lean
@@ -7,6 +7,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Yaël Dillies
 import algebra.order.group.defs
 import algebra.order.monoid.cancel.defs
 import algebra.order.monoid.canonical.defs
+import algebra.order.monoid.nat_cast
 import algebra.order.monoid.with_zero.defs
 import algebra.order.ring.lemmas
 import algebra.ring.defs
diff --git a/src/algebra/order/zero_le_one.lean b/src/algebra/order/zero_le_one.lean
new file mode 100644
index 0000000000000..74413dee92bfc
--- /dev/null
+++ b/src/algebra/order/zero_le_one.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
+-/
+import order.basic
+import algebra.ne_zero
+
+/-!
+# Typeclass expressing `0 ≤ 1`.
+-/
+
+variables {α : Type*}
+
+open function
+
+/-- Typeclass for expressing that the `0` of a type is less or equal to its `1`. -/
+class zero_le_one_class (α : Type*) [has_zero α] [has_one α] [has_le α] :=
+(zero_le_one : (0 : α) ≤ 1)
+
+/-- `zero_le_one` with the type argument implicit. -/
+@[simp] lemma zero_le_one [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
+zero_le_one_class.zero_le_one
+
+/-- `zero_le_one` with the type argument explicit. -/
+lemma zero_le_one' (α) [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
+zero_le_one
+
+section
+variables [has_zero α] [has_one α] [partial_order α] [zero_le_one_class α] [ne_zero (1 : α)]
+
+/-- See `zero_lt_one'` for a version with the type explicit. -/
+@[simp] lemma zero_lt_one : (0 : α) < 1 := zero_le_one.lt_of_ne (ne_zero.ne' 1)
+
+variables (α)
+
+/-- See `zero_lt_one` for a version with the type implicit. -/
+lemma zero_lt_one' : (0 : α) < 1 := zero_lt_one
+
+end
+
+alias zero_lt_one ← one_pos
diff --git a/src/combinatorics/set_family/kleitman.lean b/src/combinatorics/set_family/kleitman.lean
index 9c8e39d497dcf..3fe9a533bc0c8 100644
--- a/src/combinatorics/set_family/kleitman.lean
+++ b/src/combinatorics/set_family/kleitman.lean
@@ -72,6 +72,6 @@ begin
   refine mul_le_mul_left' _ _,
   refine (add_le_add_left (ih ((card_le_of_subset $ subset_cons _).trans hs) _ $ λ i hi,
     (hf₁ _ $ subset_cons _ hi).2.2) _).trans _,
-  rw [mul_tsub, two_mul, ←pow_succ, ←add_tsub_assoc_of_le (pow_le_pow' (@one_le_two ℕ _ _ _ _ _)
+  rw [mul_tsub, two_mul, ←pow_succ, ←add_tsub_assoc_of_le (pow_le_pow' (one_le_two : (1 : ℕ) ≤ 2)
     tsub_le_self), tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right],
 end