Trigger CI for leanprover-community/batteries#1066

Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Martin Dvorak
 -/
 import Mathlib.Algebra.Order.Monoid.Defs
-import Mathlib.Order.BoundedOrder
+import Mathlib.Order.BoundedOrder.Lattice
 
 /-!
 # Do not combine OrderedCancelAddCommMonoid with BoundedOrder

Mathlib.lean

@@ -1035,6 +1035,8 @@ import Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
 import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
 import Mathlib.AlgebraicTopology.MooreComplex
 import Mathlib.AlgebraicTopology.Quasicategory.Basic
+import Mathlib.AlgebraicTopology.Quasicategory.Nerve
+import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
 import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
@@ -2903,6 +2905,7 @@ import Mathlib.Deprecated.LazyList
 import Mathlib.Deprecated.Logic
 import Mathlib.Deprecated.MinMax
 import Mathlib.Deprecated.NatLemmas
+import Mathlib.Deprecated.Order
 import Mathlib.Deprecated.RelClasses
 import Mathlib.Deprecated.Ring
 import Mathlib.Deprecated.Subfield
@@ -3885,7 +3888,9 @@ import Mathlib.Order.BooleanAlgebra
 import Mathlib.Order.BooleanGenerators
 import Mathlib.Order.Booleanisation
 import Mathlib.Order.Bounded
-import Mathlib.Order.BoundedOrder
+import Mathlib.Order.BoundedOrder.Basic
+import Mathlib.Order.BoundedOrder.Lattice
+import Mathlib.Order.BoundedOrder.Monotone
 import Mathlib.Order.Bounds.Basic
 import Mathlib.Order.Bounds.Defs
 import Mathlib.Order.Bounds.Image

Mathlib/Algebra/Associated/Basic.lean

@@ -8,9 +8,9 @@ import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.Group.Commute.Units
 import Mathlib.Algebra.Group.Units.Equiv
-import Mathlib.Order.BoundedOrder
 import Mathlib.Algebra.Ring.Units
 import Mathlib.Algebra.Prime.Lemmas
+import Mathlib.Order.BoundedOrder.Basic
 
 /-!
 # Associated elements.

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Units.Basic
 import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 import Mathlib.Algebra.NeZero
-import Mathlib.Order.BoundedOrder
+import Mathlib.Order.BoundedOrder.Basic
 
 /-!
 # Canonically ordered monoids

Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
-import Mathlib.Order.BoundedOrder
 import Mathlib.Algebra.Group.TypeTags.Basic
+import Mathlib.Order.BoundedOrder.Basic
 
 /-! # Ordered monoid structures on `Multiplicative α` and `Additive α`. -/
 

Mathlib/AlgebraicTopology/Quasicategory/Basic.lean

@@ -13,7 +13,7 @@ In this file we define quasicategories,
 a common model of infinity categories.
 We show that every Kan complex is a quasicategory.
 
-In `Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean`
+In `Mathlib/AlgebraicTopology/Quasicategory/Nerve.lean`,
 we show that the nerve of a category is a quasicategory.
 
 ## TODO

Mathlib/AlgebraicTopology/Quasicategory/Nerve.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2024 Nick Ward. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Emily Riehl, Nick Ward
+-/
+import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
+
+/-!
+# The nerve of a category is a quasicategory
+
+In `AlgebraicTopology.Quasicategory.StrictSegal`, we show that any
+strict Segal simplicial set is a quasicategory.
+In `AlgebraicTopology.SimplicialSet.StrictSegal`, we show that the nerve of a
+category satisfies the strict Segal condition.
+
+In this file, we prove as a direct consequence that the nerve of a category is
+a quasicategory.
+-/
+
+universe v u
+
+open CategoryTheory SSet
+
+namespace Nerve
+
+/-- By virtue of satisfying the `StrictSegal` condition, the nerve of a
+category is a `Quasicategory`. -/
+instance quasicategory {C : Type u} [Category.{v} C] :
+  Quasicategory (nerve C) := inferInstance
+
+end Nerve

Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2024 Nick Ward. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Emily Riehl, Nick Ward
+-/
+import Mathlib.AlgebraicTopology.Quasicategory.Basic
+import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
+
+/-!
+# Strict Segal simplicial sets are quasicategories
+
+In `AlgebraicTopology.SimplicialSet.StrictSegal`, we define the strict Segal
+condition on a simplicial set `X`. We say that `X` is strict Segal if its
+simplices are uniquely determined by their spine.
+
+In this file, we prove that any simplicial set satisfying the strict Segal
+condition is a quasicategory.
+-/
+
+universe u
+
+open CategoryTheory
+open Simplicial SimplicialObject SimplexCategory
+
+namespace SSet.StrictSegal
+
+/-- Any `StrictSegal` simplicial set is a `Quasicategory`. -/
+instance quasicategory {X : SSet.{u}} [StrictSegal X] : Quasicategory X := by
+  apply quasicategory_of_filler X
+  intro n i σ₀ h₀ hₙ
+  use spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀
+  intro j hj
+  apply spineInjective
+  ext k
+  dsimp only [spineEquiv, spine_arrow, Function.comp_apply, Equiv.coe_fn_mk]
+  rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
+  let ksucc := k.succ.castSucc
+  obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by omega
+  · rw [← spine_arrow, spine_δ_arrow_lt _ hlt]
+    dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
+    apply congr_arg
+    simp only [horn, horn.spineId, standardSimplex, uliftFunctor, Functor.comp_obj,
+      yoneda_obj_obj, whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map,
+      standardSimplex.objEquiv, Equiv.ulift, Equiv.coe_fn_symm_mk,
+      Quiver.Hom.unop_op, horn.face_coe, Subtype.mk.injEq]
+    rw [mkOfSucc_δ_lt hlt]
+    rfl
+  · rw [← spine_arrow, spine_δ_arrow_gt _ hgt]
+    dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
+    apply congr_arg
+    simp only [horn, horn.spineId, standardSimplex, uliftFunctor, Functor.comp_obj,
+      yoneda_obj_obj, whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map,
+      standardSimplex.objEquiv, Equiv.ulift, Equiv.coe_fn_symm_mk,
+      Quiver.Hom.unop_op, horn.face_coe, Subtype.mk.injEq]
+    rw [mkOfSucc_δ_gt hgt]
+    rfl
+  · /- The only inner horn of `Δ[2]` does not contain the diagonal edge. -/
+    have hn0 : n ≠ 0 := by
+      rintro rfl
+      obtain rfl : k = 0 := by omega
+      fin_cases i <;> contradiction
+    /- We construct the triangle in the standard simplex as a 2-simplex in
+    the horn. While the triangle is not contained in the inner horn `Λ[2, 1]`,
+    we can inhabit `Λ[n + 2, i] _[2]` by induction on `n`. -/
+    let triangle : Λ[n + 2, i] _[2] := by
+      cases n with
+      | zero => contradiction
+      | succ _ => exact horn.primitiveTriangle i h₀ hₙ k (by omega)
+    /- The interval spanning from `k` to `k + 2` is equivalently the spine
+    of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
+    have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by omega) =
+        X.spine 2 (σ₀.app _ triangle) := by
+      ext m
+      dsimp [spine_arrow, Path.interval, Path.map]
+      rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
+      apply congr_arg
+      simp only [horn, standardSimplex, uliftFunctor, Functor.comp_obj,
+        whiskering_obj_obj_obj, yoneda_obj_obj, uliftFunctor_obj, ne_eq,
+        whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map, len_mk,
+        Nat.reduceAdd, Quiver.Hom.unop_op]
+      cases n with
+      | zero => contradiction
+      | succ _ => ext x; fin_cases x <;> fin_cases m <;> rfl
+    rw [← spine_arrow, spine_δ_arrow_eq _ heq, hi]
+    simp only [spineToDiagonal, diagonal, spineToSimplex_spine]
+    rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
+    apply congr_arg
+    simp only [horn, standardSimplex, uliftFunctor, Functor.comp_obj,
+      whiskering_obj_obj_obj, yoneda_obj_obj, uliftFunctor_obj,
+      uliftFunctor_map, whiskering_obj_obj_map, yoneda_obj_map, horn.face_coe,
+      len_mk, Nat.reduceAdd, Quiver.Hom.unop_op, Subtype.mk.injEq, ULift.up_inj]
+    ext z
+    cases n with
+    | zero => contradiction
+    | succ _ =>
+      fin_cases z <;>
+      · simp only [standardSimplex.objEquiv, uliftFunctor_map, yoneda_obj_map,
+          Quiver.Hom.unop_op, Equiv.ulift_symm_down]
+        rw [mkOfSucc_δ_eq heq]
+        rfl
+
+end SSet.StrictSegal

Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Emily Riehl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Emily Riehl, Joël Riou, Johan Commelin, Nick Ward
 -/
-import Mathlib.AlgebraicTopology.Quasicategory.Basic
 import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
 import Mathlib.AlgebraicTopology.SimplicialSet.Path
 import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
@@ -153,81 +152,6 @@ lemma spine_δ_arrow_eq (f : Path X (n + 1)) {i : Fin n} {j : Fin (n + 2)}
   rw [← FunctorToTypes.map_comp_apply, ← op_comp]
   rw [mkOfSucc_δ_eq h, spineToSimplex_edge]
 
-/-- Any `StrictSegal` simplicial set is a `Quasicategory`. -/
-instance : Quasicategory X := by
-  apply quasicategory_of_filler X
-  intro n i σ₀ h₀ hₙ
-  use spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀
-  intro j hj
-  apply spineInjective
-  ext k
-  · dsimp only [spineEquiv, spine_arrow, Function.comp_apply, Equiv.coe_fn_mk]
-    rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
-    let ksucc := k.succ.castSucc
-    obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by omega
-    · rw [← spine_arrow, spine_δ_arrow_lt _ hlt]
-      dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
-      apply congr_arg
-      simp only [horn, horn.spineId, standardSimplex, uliftFunctor, Functor.comp_obj,
-        yoneda_obj_obj, whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map,
-        standardSimplex.objEquiv, Equiv.ulift, Equiv.coe_fn_symm_mk,
-        Quiver.Hom.unop_op, horn.face_coe, Subtype.mk.injEq]
-      rw [mkOfSucc_δ_lt hlt]
-      rfl
-    · rw [← spine_arrow, spine_δ_arrow_gt _ hgt]
-      dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
-      apply congr_arg
-      simp only [horn, horn.spineId, standardSimplex, uliftFunctor, Functor.comp_obj,
-        yoneda_obj_obj, whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map,
-        standardSimplex.objEquiv, Equiv.ulift, Equiv.coe_fn_symm_mk,
-        Quiver.Hom.unop_op, horn.face_coe, Subtype.mk.injEq]
-      rw [mkOfSucc_δ_gt hgt]
-      rfl
-    · /- The only inner horn of `Δ[2]` does not contain the diagonal edge. -/
-      have hn0 : n ≠ 0 := by
-        rintro rfl
-        obtain rfl : k = 0 := by omega
-        fin_cases i <;> contradiction
-      /- We construct the triangle in the standard simplex as a 2-simplex in
-      the horn. While the triangle is not contained in the inner horn `Λ[2, 1]`,
-      we can inhabit `Λ[n + 2, i] _[2]` by induction on `n`. -/
-      let triangle : Λ[n + 2, i] _[2] := by
-        cases n with
-        | zero => contradiction
-        | succ _ => exact horn.primitiveTriangle i h₀ hₙ k (by omega)
-      /- The interval spanning from `k` to `k + 2` is equivalently the spine
-      of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
-      have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by omega) =
-          X.spine 2 (σ₀.app _ triangle) := by
-        ext m
-        dsimp [spine_arrow, Path.interval, Path.map]
-        rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
-        apply congr_arg
-        simp only [horn, standardSimplex, uliftFunctor, Functor.comp_obj,
-          whiskering_obj_obj_obj, yoneda_obj_obj, uliftFunctor_obj, ne_eq,
-          whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map, len_mk,
-          Nat.reduceAdd, Quiver.Hom.unop_op]
-        cases n with
-        | zero => contradiction
-        | succ _ => ext x; fin_cases x <;> fin_cases m <;> rfl
-      rw [← spine_arrow, spine_δ_arrow_eq _ heq, hi]
-      simp only [spineToDiagonal, diagonal, spineToSimplex_spine]
-      rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
-      apply congr_arg
-      simp only [horn, standardSimplex, uliftFunctor, Functor.comp_obj,
-        whiskering_obj_obj_obj, yoneda_obj_obj, uliftFunctor_obj,
-        uliftFunctor_map, whiskering_obj_obj_map, yoneda_obj_map, horn.face_coe,
-        len_mk, Nat.reduceAdd, Quiver.Hom.unop_op, Subtype.mk.injEq, ULift.up_inj]
-      ext z
-      cases n with
-      | zero => contradiction
-      | succ _ =>
-        fin_cases z <;>
-        · simp only [standardSimplex.objEquiv, uliftFunctor_map, yoneda_obj_map,
-            Quiver.Hom.unop_op, Equiv.ulift_symm_down]
-          rw [mkOfSucc_δ_eq heq]
-          rfl
-
 end StrictSegal
 
 end SSet
@@ -260,8 +184,4 @@ noncomputable instance strictSegal (C : Type u) [Category.{v} C] : StrictSegal (
     · intro i hi
       apply ComposableArrows.mkOfObjOfMapSucc_map_succ
 
-/-- By virtue of satisfying the `StrictSegal` condition, the nerve of a
-category is a `Quasicategory`. -/
-instance : Quasicategory (nerve C) := inferInstance
-
 end Nerve

Mathlib/Data/List/MinMax.lean

@@ -6,6 +6,7 @@ Authors: Minchao Wu, Chris Hughes, Mantas Bakšys
 import Mathlib.Data.List.Basic
 import Mathlib.Order.MinMax
 import Mathlib.Order.WithBot
+import Mathlib.Order.BoundedOrder.Lattice
 
 /-!
 # Minimum and maximum of lists

Mathlib/Data/PSigma/Order.lean

@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Minchao Wu
 -/
 import Mathlib.Data.Sigma.Lex
-import Mathlib.Order.BoundedOrder
 import Mathlib.Util.Notation3
 import Init.NotationExtra
 import Mathlib.Data.Sigma.Basic
+import Mathlib.Order.Lattice
+import Mathlib.Order.BoundedOrder.Basic
 
 /-!
 # Lexicographic order on a sigma type

Mathlib/Data/Prod/Lex.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Minchao Wu
 -/
 import Mathlib.Data.Prod.Basic
-import Mathlib.Order.BoundedOrder
+import Mathlib.Order.Lattice
+import Mathlib.Order.BoundedOrder.Basic
 
 /-!
 # Lexicographic order

Mathlib/Data/Sigma/Order.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Data.Sigma.Lex
-import Mathlib.Order.BoundedOrder
 import Mathlib.Util.Notation3
 import Mathlib.Data.Sigma.Basic
+import Mathlib.Order.Lattice
+import Mathlib.Order.BoundedOrder.Basic
 
 /-!
 # Orders on a sigma type

Mathlib/Deprecated/Order.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
+-/
+import Mathlib.Order.Defs
+
+/-!
+# Deprecated instances about order structures.
+-/
+
+variable {α : Type*}
+
+@[deprecated (since := "2024-11-26")] -- unused in Mathlib
+instance isStrictTotalOrder_of_linearOrder [LinearOrder α] : IsStrictTotalOrder α (· < ·) where
+  irrefl := lt_irrefl
+  trichotomous := lt_trichotomy