-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.mk.injEq : ∀ {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)