-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.mk.inj : ∀ {X : SSet} {n : ℕ}
  {concat :
    (x : X.obj (Opposite.op { len := 1 })) →
      (s : X.obj (Opposite.op { len := n })) →
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
            (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s →
          X.obj (Opposite.op { len := n + 1 })}
  {map_mkOfSucc_zero_concat :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
      (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) (concat x s h) = x}
  {δ₀_concat :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) (concat x s h) = s}
  {injective :
    ∀ {x y : X.obj (Opposite.op { len := n + 1 })},
      (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) y →
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) y →
          x = y}
  {concat_1 :
    (x : X.obj (Opposite.op { len := 1 })) →
      (s : X.obj (Opposite.op { len := n })) →
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
            (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s →
          X.obj (Opposite.op { len := n + 1 })}
  {map_mkOfSucc_zero_concat_1 :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
      (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) (concat_1 x s h) = x}
  {δ₀_concat_1 :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) (concat_1 x s h) = s}
  {injective_1 :
    ∀ {x y : X.obj (Opposite.op { len := n + 1 })},
      (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) y →
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) y →
          x = y},
  { concat := concat, map_mkOfSucc_zero_concat := map_mkOfSucc_zero_concat, δ₀_concat := δ₀_concat,
        injective := injective } =
      { concat := concat_1, map_mkOfSucc_zero_concat := map_mkOfSucc_zero_concat_1, δ₀_concat := δ₀_concat_1,
        injective := injective_1 } →
    concat = concat_1