-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.mk.injEq : ∀ {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)