-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject.Augmented C}
  {s' : X.right ⟶ X.left.obj (Opposite.op { len := 0 })}
  {s : (n : ℕ) → X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 })}
  {s'_comp_ε :
    autoParam
      (CategoryTheory.CategoryStruct.comp s' (X.hom.app (Opposite.op { len := 0 })) =
        CategoryTheory.CategoryStruct.id X.right)
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε._autoParam}
  {s₀_comp_δ₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (s 0) (X.left.δ 1) =
        CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) s')
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁._autoParam}
  {s_comp_δ₀ :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (s n) (X.left.δ 0) =
          CategoryTheory.CategoryStruct.id (X.left.obj (Opposite.op { len := n })))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀._autoParam}
  {s_comp_δ :
    autoParam
      (∀ (n : ℕ) (i : Fin (n + 2)),
        CategoryTheory.CategoryStruct.comp (s (n + 1)) (X.left.δ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.left.δ i) (s n))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ._autoParam}
  {s_comp_σ :
    autoParam
      (∀ (n : ℕ) (i : Fin (n + 1)),
        CategoryTheory.CategoryStruct.comp (s n) (X.left.σ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.left.σ i) (s (n + 1)))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ._autoParam}
  {s'_1 : X.right ⟶ X.left.obj (Opposite.op { len := 0 })}
  {s_1 : (n : ℕ) → X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 })}
  {s'_comp_ε_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp s'_1 (X.hom.app (Opposite.op { len := 0 })) =
        CategoryTheory.CategoryStruct.id X.right)
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε._autoParam}
  {s₀_comp_δ₁_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (s_1 0) (X.left.δ 1) =
        CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) s'_1)
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁._autoParam}
  {s_comp_δ₀_1 :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (s_1 n) (X.left.δ 0) =
          CategoryTheory.CategoryStruct.id (X.left.obj (Opposite.op { len := n })))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀._autoParam}
  {s_comp_δ_1 :
    autoParam
      (∀ (n : ℕ) (i : Fin (n + 2)),
        CategoryTheory.CategoryStruct.comp (s_1 (n + 1)) (X.left.δ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.left.δ i) (s_1 n))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ._autoParam}
  {s_comp_σ_1 :
    autoParam
      (∀ (n : ℕ) (i : Fin (n + 1)),
        CategoryTheory.CategoryStruct.comp (s_1 n) (X.left.σ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.left.σ i) (s_1 (n + 1)))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ._autoParam},
  { s' := s', s := s, s'_comp_ε := s'_comp_ε, s₀_comp_δ₁ := s₀_comp_δ₁, s_comp_δ₀ := s_comp_δ₀, s_comp_δ := s_comp_δ,
        s_comp_σ := s_comp_σ } =
      { s' := s'_1, s := s_1, s'_comp_ε := s'_comp_ε_1, s₀_comp_δ₁ := s₀_comp_δ₁_1, s_comp_δ₀ := s_comp_δ₀_1,
        s_comp_δ := s_comp_δ_1, s_comp_σ := s_comp_σ_1 } →
    s' = s'_1 ∧ s = s_1