Mathlib SSet: pointed simplices of dim ≥ 2 in a strict Segal set (nerve) are constant, ~25 lines

To show π_{n+2} of a nerve vanishes using Mathlib's PtSimplex (maps Δ[m] ⟶ X sending ∂Δ[m] to x): prove f = .const by RelativeMorphism.ext (yonedaEquiv.injective ((IsStrictSegal.segal (n+2)).1 ?_)), then ext i : 1 on the Path (Path.ext' compares arrows only) reduces to X.map θ.op (yonedaEquiv f.map) = X.map θ.op (yonedaEquiv (const x)) for θ : ⦋1⦌ ⟶ ⦋n+2⦌. Use naturality X.map θ.op (yonedaEquiv φ) = yonedaEquiv (stdSimplex.map θ ≫ φ), proved as (ConcreteCategory.congr_hom (φ.naturality θ.op) _).symm. θ is not surjective by Fintype.card_le_of_surjective. SimplexCategory.eq_comp_δ_of_not_surjective factors it as θ' ≫ δ i, and PtSimplex.δ_map kills stdSimplex.δ i ≫ f.map. rw [Functor.map_comp, Category.assoc] turns stdSimplex.map (θ' ≫ δ i) into a composite with stdSimplex.δ i (rfl-compatible).