chore: prevent API leakage on SimplexCategory (#11395)

This PR removes the `simps` attribute in the definition of the category structure on `SimplexCategory` so as to prevent API leakage. Better suited `simp` lemmas are added. The definition of `SimplexCategory.const` is also generalized in order to describe any constant map in `SimplexCategory`.

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -127,7 +127,7 @@ def equivalenceLeftToRight (X : SimplicialObject.Augmented C) (F : Arrow C)
   left :=
     { app := fun x =>
         Limits.WidePullback.lift (X.hom.app _ ≫ G.right)
-          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) fun i => by
+          (fun i => X.left.map (SimplexCategory.const _ x.unop i).op ≫ G.left) fun i => by
           dsimp
           erw [Category.assoc, Arrow.w, Augmented.toArrow_obj_hom, NatTrans.naturality_assoc,
             Functor.const_obj_map, Category.id_comp]
@@ -284,11 +284,11 @@ def equivalenceRightToLeft (F : Arrow C) (X : CosimplicialObject.Augmented C)
   right :=
     { app := fun x =>
         Limits.WidePushout.desc (G.left ≫ X.hom.app _)
-          (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
+          (fun i => G.right ≫ X.right.map (SimplexCategory.const _ x i))
           (by
             rintro j
             rw [← Arrow.w_assoc G]
-            have t := X.hom.naturality (x.const j)
+            have t := X.hom.naturality (SimplexCategory.const (SimplexCategory.mk 0) x j)
             dsimp at t ⊢
             simp only [Category.id_comp] at t
             rw [← t])

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -146,27 +146,42 @@ def comp {a b c : SimplexCategory} (f : SimplexCategory.Hom b c) (g : SimplexCat
 
 end Hom
 
-@[simps]
 instance smallCategory : SmallCategory.{0} SimplexCategory where
   Hom n m := SimplexCategory.Hom n m
   id m := SimplexCategory.Hom.id _
   comp f g := SimplexCategory.Hom.comp g f
 #align simplex_category.small_category SimplexCategory.smallCategory
 
+@[simp]
+lemma id_toOrderHom (a : SimplexCategory) :
+    Hom.toOrderHom (𝟙 a) = OrderHom.id := rfl
+
+@[simp]
+lemma comp_toOrderHom {a b c: SimplexCategory} (f : a ⟶ b) (g : b ⟶ c) :
+    (f ≫ g).toOrderHom = g.toOrderHom.comp f.toOrderHom := rfl
+
 -- Porting note: added because `Hom.ext'` is not triggered automatically
 @[ext]
 theorem Hom.ext {a b : SimplexCategory} (f g : a ⟶ b) :
     f.toOrderHom = g.toOrderHom → f = g :=
   Hom.ext' _ _
 
 /-- The constant morphism from [0]. -/
-def const (x : SimplexCategory) (i : Fin (x.len + 1)) : ([0] : SimplexCategory) ⟶ x :=
+def const (x y : SimplexCategory) (i : Fin (y.len + 1)) : x ⟶ y :=
   Hom.mk <| ⟨fun _ => i, by tauto⟩
 #align simplex_category.const SimplexCategory.const
 
--- Porting note: removed @[simp] as the linter complains
-theorem const_comp (x y : SimplexCategory) (i : Fin (x.len + 1)) (f : x ⟶ y) :
-    const x i ≫ f = const y (f.toOrderHom i) :=
+@[simp]
+lemma const_eq_id : const [0] [0] 0 = 𝟙 _ := by aesop
+
+@[simp]
+lemma const_apply (x y : SimplexCategory) (i : Fin (y.len + 1)) (a : Fin (x.len + 1)) :
+    (const x y i).toOrderHom a = i := rfl
+
+@[simp]
+theorem const_comp (x : SimplexCategory) {y z : SimplexCategory}
+    (f : y ⟶ z) (i : Fin (y.len + 1)) :
+    const x y i ≫ f = const x z (f.toOrderHom i) :=
   rfl
 #align simplex_category.const_comp SimplexCategory.const_comp
 
@@ -663,8 +678,8 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
     ∃ θ' : mk n ⟶ Δ', θ = σ i ≫ θ' := by
   use δ i.succ ≫ θ
   ext1; ext1; ext1 x
-  simp only [Hom.toOrderHom_mk, Function.comp_apply, OrderHom.comp_coe, Hom.comp,
-    smallCategory_comp, σ, mkHom, OrderHom.coe_mk]
+  simp only [len_mk, σ, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
+    OrderHom.coe_mk, Function.comp_apply]
   by_cases h' : x ≤ Fin.castSucc i
   · -- This was not needed before leanprover/lean4#2644
     dsimp
@@ -732,12 +747,9 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
     ext1
     ext1
     ext1 x
-    simp only [Hom.toOrderHom_mk, Function.comp_apply, OrderHom.comp_coe, Hom.comp,
-      smallCategory_comp]
+    simp only [len_mk, Category.assoc, comp_toOrderHom, OrderHom.comp_coe, Function.comp_apply]
     by_cases h' : θ.toOrderHom x ≤ i
     · simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk]
-      -- This was not needed before leanprover/lean4#2644
-      dsimp
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
       erw [Fin.predAbove_of_le_castSucc _ _ (by rwa [Fin.castSucc_castPred])]
       dsimp [δ]
@@ -746,15 +758,11 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
       · rw [(hi x).le_iff_lt] at h'
         exact h'
     · simp only [not_le] at h'
-      -- The next three tactics used to be a simp only call before leanprover/lean4#2644
-      rw [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk, OrderHom.coe_mk]
-      erw [OrderHom.coe_mk]
+      dsimp [σ, δ]
       erw [Fin.predAbove_of_castSucc_lt _ _ (by rwa [Fin.castSucc_castPred])]
-      dsimp [δ]
       rw [Fin.succAbove_of_le_castSucc i _]
       erw [Fin.succ_pred]
-      simpa only [Fin.le_iff_val_le_val, Fin.coe_castSucc, Fin.coe_pred] using
-        Nat.le_sub_one_of_lt (Fin.lt_iff_val_lt_val.mp h')
+      exact Nat.le_sub_one_of_lt (Fin.lt_iff_val_lt_val.mp h')
   · obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h)
     use θ ≫ σ (Fin.last _)
     ext x : 3

Mathlib/AlgebraicTopology/SimplicialObject.lean

@@ -388,7 +388,7 @@ def augment (X : SimplicialObject C) (X₀ : C) (f : X _[0] ⟶ X₀)
   left := X
   right := X₀
   hom :=
-    { app := fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f
+    { app := fun i => X.map (SimplexCategory.const _ _ 0).op ≫ f
       naturality := by
         intro i j g
         dsimp
@@ -398,9 +398,7 @@ def augment (X : SimplicialObject C) (X₀ : C) (f : X _[0] ⟶ X₀)
 
 -- Porting note: removed @[simp] as the linter complains
 theorem augment_hom_zero (X : SimplicialObject C) (X₀ : C) (f : X _[0] ⟶ X₀) (w) :
-    (X.augment X₀ f w).hom.app (op [0]) = f := by
-  dsimp
-  rw [SimplexCategory.hom_zero_zero ([0].const 0), op_id, X.map_id, Category.id_comp]
+    (X.augment X₀ f w).hom.app (op [0]) = f := by simp
 #align category_theory.simplicial_object.augment_hom_zero CategoryTheory.SimplicialObject.augment_hom_zero
 
 end SimplicialObject
@@ -753,18 +751,16 @@ def augment (X : CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.obj [0])
   left := X₀
   right := X
   hom :=
-    { app := fun i => f ≫ X.map (SimplexCategory.const i 0)
+    { app := fun i => f ≫ X.map (SimplexCategory.const _ _ 0)
       naturality := by
         intro i j g
         dsimp
-        simpa [← X.map_comp] using w _ _ _ }
+        rw [Category.id_comp, Category.assoc, ← X.map_comp, w] }
 #align category_theory.cosimplicial_object.augment CategoryTheory.CosimplicialObject.augment
 
 -- Porting note: removed @[simp] as the linter complains
 theorem augment_hom_zero (X : CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.obj [0]) (w) :
-    (X.augment X₀ f w).hom.app [0] = f := by
-  dsimp
-  rw [SimplexCategory.hom_zero_zero ([0].const 0), X.map_id, Category.comp_id]
+    (X.augment X₀ f w).hom.app [0] = f := by simp
 #align category_theory.cosimplicial_object.augment_hom_zero CategoryTheory.CosimplicialObject.augment_hom_zero
 
 end CosimplicialObject