feat(AlgebraicTopology/SimplicialSet): homotopy groups of Kan complexes

[joelriou]

WIP

---

• depends on: feat(AlgebraicTopology/SimplicialSet): MulStruct.nonempty #42474
• depends on: feat(AlgebraicTopology): the truncated quasicategory induced by a quasicategory #42473
• depends on: feat(AlgebraicTopology/SimplicialSet): construction of morphisms from Δ[p] ⊗ Δ[1]  #42295
• depends on: feat(AlgebraicTopology): pushout diagrams in the filtration of Δ[p] ⊗ Δ[1] #41675
• depends on: feat(AlgebraicTopology): order relation between simplices of the nerve of a partial order #41656
• depends on: feat(AlgebraicTopology): filtration of Δ[p] ⊗ Δ[1] #41655
• depends on: feat(AlgebraicTopology): non-degenerate simplices in Δ[p] ⊗ Δ[q] #41624
• depends on: feat(Order/Fin): conditions for Fin.insertNth to be monotone or strictly monotone #41617
• depends on: feat(AlgebraicTopology/SimplicialSet/KanComplex): MulStruct.assoc #38216
• depends on: feat(AlgebraicTopology/SimplicialSet): more API for SSet.op #38664
• depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): characterization of Kan complexes #38665
• depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): faces of the boundary #38662
• depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul #38172
• depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): morphisms from horns #38367
• depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): the opposite of a horn #38063

[github-actions]

PR summary a5a54ebb28

Import changes exceeding 2%

%	File
+6.26%	Mathlib.AlgebraicTopology.SimplicialSet.Boundary
+9.47%	Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct	1003	1098	+95 (+9.47%)
Mathlib.AlgebraicTopology.SimplicialSet.Boundary	942	1001	+59 (+6.26%)
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex	1089	1096	+7 (+0.64%)

Import changes for all files

Files	Import difference
14 files Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex	2
9 files Mathlib.AlgebraicTopology.SimplicialSet.CompStruct Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.Homotopy Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.Topology.Homotopy.TopCat.ToSSet	3
6 files Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.InnerFibration Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.KanComplex	7
Mathlib.AlgebraicTopology.SimplicialSet.Skeleton	13
Mathlib.AlgebraicTopology.SimplicialSet.Boundary	59
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct	95
Mathlib.Order.Fin.InsertNth (new file)	371
Mathlib.Order.Fin.Prod (new file)	390
Mathlib.AlgebraicTopology.Quasicategory.TwoTruncatedQuasicategory (new file)	1099
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.FundamentalGroupoid (new file)	1102
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.PtSimplexEquiv (new file)	1110
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.HomotopyGroup (new file)	1111

---

Declarations diff (regex)

+ CompStruct.homInvId
+ CompStruct.invHomId
+ CompStruct.nonempty_iff
+ FundamentalGroupoid
+ Homotopy
+ MulStruct.unique
+ MulStruct.unique'
+ PtSimplex.MulStruct.mul_eq
+ RelStruct₀
+ RelStruct₀.homotopy
+ _root_.SSet.ι₀_stdSimplex_zero
+ _root_.SSet.ι₁_stdSimplex_zero
+ assoc
+ assoc'
+ assocAux
+ cases_last
+ cases_one
+ codimOneSimplex
+ exists_desc
+ exists_nonDegenerate_max_dim
+ exists_nonDegenerate_max_dim_aux
+ filtration
+ filtration.bicartSq
+ filtration.exists_desc
+ filtration.isPushout
+ filtration.ι
+ filtration.ι_ι
+ filtration_last
+ filtration_monotone
+ filtration_zero
+ fst_apply
+ fst_rightUnitor_inv
+ group
+ group'
+ homMk
+ homMk_fac_of_compStruct
+ homMk_id
+ homMk_inv
+ homMk_surjective
+ hom_ext_tensorLeft
+ hom_ext_tensorRight
+ hom_ext₀_tensorLeft
+ hom_ext₀_tensorRight
+ hom_rec
+ image_le_image_iff
+ insertNth_last_monotone
+ insertNth_monotone
+ insertNth_zero_monotone
+ instance (X : SSet.{u}) [X.Quasicategory] :
+ instance (i : Fin (p + 1)) : Mono (ι.{u} i) := Nonsingular.mono _
+ instance : Category (FundamentalGroupoid X)
+ instance : IsGroupoid (FundamentalGroupoid X) := by
+ instance : One (π n X x)
+ instance {X : SSet.{u}} [KanComplex X] : KanComplex X.op := by
+ intersectionNondeg
+ intersectionNondeg_le_intersectionNondeg
+ intersectionNondeg_le_intersectionNondeg'
+ inv_mul
+ isCompatible_α
+ isGroupoid_aux
+ isGroupoid_aux'
+ isoNerve_hom_app_obj
+ isoOfRepresentableBy_ofSimplexRepresentableBy_hom
+ leftUnitor
+ leftUnitor_hom_naturality
+ leftUnitor_inv_map_δ_one
+ leftUnitor_inv_map_δ_zero
+ leftUnitor_inv_naturality
+ leftUnitor_inv_snd
+ map_eq_const_equiv₀
+ mem_range_objEquiv_nonDegenerateEquiv₀_iff
+ mem_range_objEquiv_nonDegenerateEquiv₁_iff
+ mk
+ mk_eq_mk_iff
+ mk_eq_one_iff
+ mk_surjective
+ mul
+ mul'
+ mulOneEqOfOneMulEq
+ mulOneEqSymm
+ mulOneEqTrans
+ mulStruct
+ mul_assoc
+ mul_eq_of_mulStruct
+ mul_eq_of_mulStruct'
+ mul_mk_eq_iff'
+ mul_one
+ nerve_ofSimplex_le_ofSimplex_iff
+ nonDegenerateEquiv
+ nonDegenerateEquiv_fst
+ nonDegenerateEquiv_snd
+ nonDegenerate_of_app_apply
+ nonempty
+ objEquiv
+ objEquiv_apply_symm_apply
+ objEquiv_symm_δ_apply
+ objEquiv_symm_σ_apply
+ objMk
+ ofSimplexRepresentableBy
+ ofSimplexRepresentableBy_id
+ ofSimplex_codimOneSimplex
+ ofSimplex_le_filtration
+ ofSimplex_le_ofSimplex_iff
+ ofSucc
+ on
+ oneMulEqOfMulOneEq
+ oneMulEqSymm
+ oneMulEqTrans
+ one_mul
+ opEquiv
+ opObjEquiv_symm_yonedaEquiv_const
+ opObjEquiv_yonedaEquiv_const
+ op_edge
+ op_simplex
+ op_unop
+ preimage_image
+ preimage_monotone
+ prodStdSimplex.nonDegenerateEquiv₁
+ prodStdSimplex.nonDegenerateEquiv₁_fst
+ prodStdSimplex.nonDegenerateEquiv₂_snd
+ prod_exists_lt_lt_of_le_of_le
+ prod_lt_last_last_iff
+ prod_zero_zero_lt_iff
+ range_isoNerve_hom_app_obj
+ refl
+ relStruct
+ rightUnitor
+ rightUnitor_hom_naturality
+ rightUnitor_hom_ι₀
+ rightUnitor_hom_ι₁
+ rightUnitor_inv_fst
+ rightUnitor_inv_map_δ_one
+ rightUnitor_inv_map_δ_zero
+ rightUnitor_inv_naturality
+ snd_apply
+ snd_leftUnitor_inv
+ src
+ src_succ
+ src_zero
+ stdSimplex.yonedaEquiv_δ_comp
+ stdSimplex.yonedaEquiv_σ_comp
+ stdSimplex.δ_comp_yonedaEquiv_symm
+ stdSimplex.σ_comp_yonedaEquiv_symm
+ strictMono_insertNth
+ strictMono_insertNth_last
+ strictMono_insertNth_zero
+ subcomplex_eq_top_iff
+ succ
+ tgt
+ tgt_last
+ toOfSimplex_app_objEquiv_symm
+ unop_edge
+ unop_op
+ unop_simplex
+ yonedaEquiv_fst
+ yonedaEquiv_isoOfRepresentableBy_hom
+ yonedaEquiv_isoOfRepresentableBy_ofSimplexRepresentableBy_hom
+ yonedaEquiv_snd
+ yonedaEquiv_symm_comp
+ yonedaEquiv_symm_map
+ yonedaEquiv_ι
+ yonedaEquiv_ι₀
+ α
+ α_castSucc_castSucc_castSucc
+ α_castSucc_succ_succ
+ α_of_gt
+ α_of_lt
+ α_succ_succ_succ
+ δ_castSucc_nonDegenerateEquiv
+ δ_one_yonedaEquiv_symm
+ δ_one_yonedeEquiv_symm
+ δ_opObjEquiv
+ δ_succ_castSucc_nonDegenerateEquiv_succ
+ δ_succ_castSucc_ι_succ
+ δ_succ_nonDegenerateEquiv
+ δ_two_yonedaEquiv_symm
+ δ_whiskerRight_h_eq_const
+ δ_zero_yonedaEquiv_symm
+ δ_zero_yonedeEquiv_symm
+ δ_ι_h_eq_const_of_gt
+ δ_ι_h_eq_const_of_lt
+ δ_ι_last
+ δ_ι_of_gt
+ δ_ι_of_lt
+ δ_ι_zero
+ ι
+ ι_def
+ ι_fst
+ ι_snd
+ ι_δ_whiskerRight_of_gt
+ ι_δ_whiskerRight_of_le
+ π
+ ρ
+ σ_opObjEquiv
+ σ_zero_eq_yonedaEquiv_const
++ exists_left_inverse
++ hom_ext
++ inv
++ mem_ofSimplex_obj_iff
++ mul_mk_eq_iff
++ rec
++ relStruct₀
++ symm
++ trans
+++ equiv₀
++++ op
++++ unop
- _root_.SSet.yonedaEquiv_symm_comp
- instance : Category (CosimplicialObject C) := by
- nonDegenerateEquiv₁
- nonDegenerateEquiv₁_fst
- nonDegenerateEquiv₁_snd

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a5a54eb).

• +266 new declarations
• −4 removed declarations

(showing first 200 of 270 lines)

-CategoryTheory.CosimplicialObject.comp_app
-CategoryTheory.CosimplicialObject.id_app
-CategoryTheory.CosimplicialObject.instCategory
+Fin.insertNth.hcongr_6
+Fin.insertNth_last_monotone
+Fin.insertNth_monotone
+Fin.insertNth_zero_monotone
+Fin.prod_exists_lt_lt_of_le_of_le
+Fin.prod_lt_last_last_iff
+Fin.prod_zero_zero_lt_iff
+Fin.strictMono_insertNth
+Fin.strictMono_insertNth_last
+Fin.strictMono_insertNth_zero
+PartialOrder.nerve_ofSimplex_le_ofSimplex_iff
+SSet.Edge.CompStruct.homInvId
+SSet.Edge.CompStruct.invHomId
+SSet.Edge.CompStruct.nonempty_iff
+SSet.Edge.CompStruct.op
+SSet.Edge.CompStruct.op_simplex
+SSet.Edge.CompStruct.unop
+SSet.Edge.CompStruct.unop_simplex
+SSet.Edge.CompStruct.δ_one_yonedaEquiv_symm
+SSet.Edge.CompStruct.δ_one_yonedaEquiv_symm_assoc
+SSet.Edge.CompStruct.δ_two_yonedaEquiv_symm
+SSet.Edge.CompStruct.δ_two_yonedaEquiv_symm_assoc
+SSet.Edge.CompStruct.δ_zero_yonedaEquiv_symm
+SSet.Edge.CompStruct.δ_zero_yonedaEquiv_symm_assoc
+SSet.Edge.homMk_inv
+SSet.Edge.inv
+SSet.Edge.inv.congr_simp
+SSet.Edge.op
+SSet.Edge.op_edge
+SSet.Edge.op_unop
+SSet.Edge.unop
+SSet.Edge.unop_edge
+SSet.Edge.unop_op
+SSet.Edge.δ_one_yonedeEquiv_symm
+SSet.Edge.δ_one_yonedeEquiv_symm_assoc
+SSet.Edge.δ_zero_yonedeEquiv_symm
+SSet.Edge.δ_zero_yonedeEquiv_symm_assoc
+SSet.KanComplex.FundamentalGroupoid
+SSet.KanComplex.FundamentalGroupoid.homMk
+SSet.KanComplex.FundamentalGroupoid.homMk_fac_of_compStruct
+SSet.KanComplex.FundamentalGroupoid.homMk_fac_of_compStruct_assoc
+SSet.KanComplex.FundamentalGroupoid.homMk_id
+SSet.KanComplex.FundamentalGroupoid.homMk_surjective
+SSet.KanComplex.FundamentalGroupoid.hom_rec
+SSet.KanComplex.FundamentalGroupoid.instIsGroupoid
+SSet.KanComplex.FundamentalGroupoid.objEquiv
+SSet.KanComplex.FundamentalGroupoid.objEquiv_apply
+SSet.KanComplex.FundamentalGroupoid.objEquiv_symm_apply_pt
+SSet.KanComplex.FundamentalGroupoid.objMk
+SSet.KanComplex.FundamentalGroupoid.rec
+SSet.KanComplex.instCategoryFundamentalGroupoid
+SSet.KanComplex.π
+SSet.KanComplex.π.group
+SSet.KanComplex.π.group'
+SSet.KanComplex.π.instOne
+SSet.KanComplex.π.mk
+SSet.KanComplex.π.mk_eq_mk_iff
+SSet.KanComplex.π.mk_eq_one_iff
+SSet.KanComplex.π.mk_surjective
+SSet.KanComplex.π.mul_eq_of_mulStruct'
+SSet.KanComplex.π.mul_mk_eq_iff
+SSet.KanComplex.π.mul_mk_eq_iff'
+SSet.KanComplex.π.rec
+SSet.PtSimplex.Homotopy
+SSet.PtSimplex.Homotopy.equiv₀
+SSet.PtSimplex.Homotopy.relStruct₀
+SSet.PtSimplex.Homotopy.relStruct₀.src
+SSet.PtSimplex.Homotopy.relStruct₀.src_map
+SSet.PtSimplex.Homotopy.relStruct₀.src_succ
+SSet.PtSimplex.Homotopy.relStruct₀.src_zero
+SSet.PtSimplex.Homotopy.relStruct₀.tgt
+SSet.PtSimplex.Homotopy.relStruct₀.tgt_last
+SSet.PtSimplex.Homotopy.relStruct₀.tgt_map
+SSet.PtSimplex.Homotopy.relStruct₀.ρ
+SSet.PtSimplex.Homotopy.relStruct₀.ρ_map
+SSet.PtSimplex.Homotopy.δ_whiskerRight_h_eq_const
+SSet.PtSimplex.Homotopy.δ_whiskerRight_h_eq_const_assoc
+SSet.PtSimplex.Homotopy.δ_ι_h_eq_const_of_gt
+SSet.PtSimplex.Homotopy.δ_ι_h_eq_const_of_gt_assoc
+SSet.PtSimplex.Homotopy.δ_ι_h_eq_const_of_lt
+SSet.PtSimplex.Homotopy.δ_ι_h_eq_const_of_lt_assoc
+SSet.PtSimplex.MulStruct.assoc
+SSet.PtSimplex.MulStruct.assoc'
+SSet.PtSimplex.MulStruct.exists_left_inverse
+SSet.PtSimplex.MulStruct.mulOneEqOfOneMulEq
+SSet.PtSimplex.MulStruct.mulOneEqSymm
+SSet.PtSimplex.MulStruct.mulOneEqTrans
+SSet.PtSimplex.MulStruct.mul_eq
+SSet.PtSimplex.MulStruct.nonempty
+SSet.PtSimplex.MulStruct.oneMulEqOfMulOneEq
+SSet.PtSimplex.MulStruct.oneMulEqSymm
+SSet.PtSimplex.MulStruct.oneMulEqTrans
+SSet.PtSimplex.MulStruct.op
+SSet.PtSimplex.MulStruct.op_map
+SSet.PtSimplex.MulStruct.unique
+SSet.PtSimplex.MulStruct.unique'
+SSet.PtSimplex.MulStruct.unop
+SSet.PtSimplex.MulStruct.unop_map
+SSet.PtSimplex.RelStruct.mk.congr_simp
+SSet.PtSimplex.RelStruct.ofSucc
+SSet.PtSimplex.RelStruct.relStruct₀
+SSet.PtSimplex.RelStruct.succ
+SSet.PtSimplex.RelStruct.symm
+SSet.PtSimplex.RelStruct.symm.congr_simp
+SSet.PtSimplex.RelStruct.trans
+SSet.PtSimplex.RelStruct₀
+SSet.PtSimplex.RelStruct₀.equiv₀
+SSet.PtSimplex.RelStruct₀.homotopy
+SSet.PtSimplex.RelStruct₀.refl
+SSet.PtSimplex.RelStruct₀.relStruct
+SSet.PtSimplex.RelStruct₀.symm
+SSet.PtSimplex.RelStruct₀.symm.congr_simp
+SSet.PtSimplex.RelStruct₀.trans
+SSet.PtSimplex.cases_last
+SSet.PtSimplex.cases_one
+SSet.PtSimplex.equiv₀
+SSet.PtSimplex.equiv₀_apply
+SSet.PtSimplex.equiv₀_symm_apply_map
+SSet.PtSimplex.map_eq_const_equiv₀
+SSet.PtSimplex.op
+SSet.PtSimplex.opEquiv
+SSet.PtSimplex.opEquiv_apply_map
+SSet.PtSimplex.opEquiv_symm_apply_map
+SSet.PtSimplex.unop
+SSet.RelativeMorphism.Homotopy.mk.congr_simp
+SSet.RelativeMorphism.mk.congr_simp
+SSet.Subcomplex.eqToIso.congr_simp
+SSet.Subcomplex.hom_ext
+SSet.Subcomplex.hom_ext_iff
+SSet.Subcomplex.image_le_image_iff
+SSet.Subcomplex.isoOfRepresentableBy_ofSimplexRepresentableBy_hom
+SSet.Subcomplex.ofSimplexRepresentableBy
+SSet.Subcomplex.ofSimplexRepresentableBy.congr_simp
+SSet.Subcomplex.ofSimplexRepresentableBy_id
+SSet.Subcomplex.preimage_image
+SSet.Subcomplex.preimage_monotone
+SSet.Subcomplex.toOfSimplex_app_objEquiv_symm
+SSet.Subcomplex.yonedaEquiv_isoOfRepresentableBy_ofSimplexRepresentableBy_hom
+SSet.boundary.hom_ext_iff
+SSet.boundary.hom_ext_tensorLeft
+SSet.boundary.hom_ext_tensorLeft_iff
+SSet.boundary.hom_ext_tensorRight
+SSet.boundary.hom_ext_tensorRight_iff
+SSet.boundary.hom_ext₀_tensorLeft
+SSet.boundary.hom_ext₀_tensorLeft_iff
+SSet.boundary.hom_ext₀_tensorRight
+SSet.boundary.hom_ext₀_tensorRight_iff
+SSet.fst_apply
+SSet.instKanComplexOp
+SSet.instQuasicategory₂ObjTruncatedOfNatNatTruncationOfQuasicategory
+SSet.nonDegenerate_of_app_apply
+SSet.opObjEquiv_symm_yonedaEquiv_const
+SSet.opObjEquiv_yonedaEquiv_const
+SSet.prodStdSimplex.exists_nonDegenerate_max_dim
+SSet.prodStdSimplex.isoNerve_hom_app_obj
+SSet.prodStdSimplex.mem_ofSimplex_obj_iff
-SSet.prodStdSimplex.nonDegenerateEquiv₁_snd
+SSet.prodStdSimplex.nonDegenerateEquiv₂_snd
+SSet.prodStdSimplex.objEquiv_apply_symm_apply
+SSet.prodStdSimplex.ofSimplex_le_ofSimplex_iff
+SSet.prodStdSimplex.range_isoNerve_hom_app_obj
+SSet.prodStdSimplex.subcomplex_eq_top_iff
+SSet.prodStdSimplex₁.codimOneSimplex
+SSet.prodStdSimplex₁.codimOneSimplex_coe_fst
+SSet.prodStdSimplex₁.codimOneSimplex_coe_snd
+SSet.prodStdSimplex₁.exists_desc
+SSet.prodStdSimplex₁.filtration
+SSet.prodStdSimplex₁.filtration.bicartSq
+SSet.prodStdSimplex₁.filtration.exists_desc
+SSet.prodStdSimplex₁.filtration.isPushout
+SSet.prodStdSimplex₁.filtration.ι
+SSet.prodStdSimplex₁.filtration.ι.congr_simp
+SSet.prodStdSimplex₁.filtration.ι_ι
+SSet.prodStdSimplex₁.filtration.ι_ι_assoc
+SSet.prodStdSimplex₁.filtration_last
+SSet.prodStdSimplex₁.filtration_monotone
+SSet.prodStdSimplex₁.filtration_zero
+SSet.prodStdSimplex₁.hom_ext
+SSet.prodStdSimplex₁.hom_ext_iff
+SSet.prodStdSimplex₁.instMonoι
+SSet.prodStdSimplex₁.intersectionNondeg
+SSet.prodStdSimplex₁.intersectionNondeg_le_intersectionNondeg
+SSet.prodStdSimplex₁.intersectionNondeg_le_intersectionNondeg'
+SSet.prodStdSimplex₁.mem_range_objEquiv_nonDegenerateEquiv₀_iff
+SSet.prodStdSimplex₁.mem_range_objEquiv_nonDegenerateEquiv₁_iff
+SSet.prodStdSimplex₁.nonDegenerateEquiv
+SSet.prodStdSimplex₁.nonDegenerateEquiv_fst
+SSet.prodStdSimplex₁.nonDegenerateEquiv_snd
+SSet.prodStdSimplex₁.ofSimplex_codimOneSimplex
+SSet.prodStdSimplex₁.ofSimplex_le_filtration
+SSet.prodStdSimplex₁.yonedaEquiv_ι
+SSet.prodStdSimplex₁.yonedaEquiv_ι₀
+SSet.prodStdSimplex₁.δ_castSucc_nonDegenerateEquiv
+SSet.prodStdSimplex₁.δ_succ_castSucc_nonDegenerateEquiv_succ
+SSet.prodStdSimplex₁.δ_succ_castSucc_ι_succ
+SSet.prodStdSimplex₁.δ_succ_castSucc_ι_succ_assoc
+SSet.prodStdSimplex₁.δ_succ_nonDegenerateEquiv

---

Increase in strong tech debt: (relative, absolute) = (3.63, 0.01)

Current number	Change	Type (strong)
503	4	erw
4363	-3	backward.defeqAttrib.useBackward
6991	5	backward.isDefEq.respectTransparency
3993	6	backward.isDefEq.respectTransparency.types

Increase in weak tech debt: (relative, absolute) = (4.00, 0.00)

Current number	Change	Type (weak)
5051	4	exposed public sections

Current commit a5a54ebb28
Reference commit 9fb10993c1

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplicialSet): MulStruct.nonempty #42474
• feat(AlgebraicTopology): the truncated quasicategory induced by a quasicategory #42473
• feat(AlgebraicTopology/SimplicialSet): construction of morphisms from Δ[p] ⊗ Δ[1]  #42295
• feat(AlgebraicTopology): pushout diagrams in the filtration of Δ[p] ⊗ Δ[1] #41675
• feat(AlgebraicTopology): order relation between simplices of the nerve of a partial order #41656
• feat(AlgebraicTopology): filtration of Δ[p] ⊗ Δ[1] #41655
• feat(AlgebraicTopology): non-degenerate simplices in Δ[p] ⊗ Δ[q] #41624
• feat(Order/Fin): conditions for Fin.insertNth to be monotone or strictly monotone #41617
• feat(AlgebraicTopology/SimplicialSet/KanComplex): MulStruct.assoc #38216
• feat(AlgebraicTopology/SimplicialSet): more API for SSet.op #38664
• [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): characterization of Kan complexes #38665
• [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): faces of the boundary #38662
• [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul #38172
• [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): morphisms from horns #38367
• [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): the opposite of a horn #38063
  By Dependent Issues (🤖). Happy coding!