-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.mk.inj : ∀ {X : SSet} {A : X.Subcomplex} {ι : Type v} {dim : ι → ℕ}
  {simplex : (s : ι) → X.obj (Opposite.op { len := dim s + 1 })} {index : (s : ι) → Fin (dim s + 2)}
  {nonDegenerate₁ : ∀ (s : ι), simplex s ∈ X.nonDegenerate (dim s + 1)}
  {nonDegenerate₂ :
    ∀ (s : ι),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) ∈
        X.nonDegenerate (dim s)}
  {notMem₁ : ∀ (s : ι), simplex s ∉ A.obj (Opposite.op { len := dim s + 1 })}
  {notMem₂ :
    ∀ (s : ι),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) ∉
        A.obj (Opposite.op { len := dim s })}
  {injective_type₁' :
    ∀ {s t : ι}, { dim := dim s + 1, simplex := simplex s } = { dim := dim t + 1, simplex := simplex t } → s = t}
  {injective_type₂' :
    ∀ {s t : ι},
      { dim := dim s,
            simplex :=
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) } =
          { dim := dim t,
            simplex :=
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index t))) (simplex t) } →
        s = t}
  {type₁_ne_type₂' :
    ∀ (s t : ι),
      { dim := dim s + 1, simplex := simplex s } ≠
        { dim := dim t,
          simplex :=
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index t))) (simplex t) }}
  {surjective' :
    ∀ (x : A.N),
      ∃ s,
        x.toS = { dim := dim s + 1, simplex := simplex s } ∨
          x.toS =
            { dim := dim s,
              simplex :=
                (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) }}
  {ι_1 : Type v} {dim_1 : ι_1 → ℕ} {simplex_1 : (s : ι_1) → X.obj (Opposite.op { len := dim_1 s + 1 })}
  {index_1 : (s : ι_1) → Fin (dim_1 s + 2)}
  {nonDegenerate₁_1 : ∀ (s : ι_1), simplex_1 s ∈ X.nonDegenerate (dim_1 s + 1)}
  {nonDegenerate₂_1 :
    ∀ (s : ι_1),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index_1 s))) (simplex_1 s) ∈
        X.nonDegenerate (dim_1 s)}
  {notMem₁_1 : ∀ (s : ι_1), simplex_1 s ∉ A.obj (Opposite.op { len := dim_1 s + 1 })}
  {notMem₂_1 :
    ∀ (s : ι_1),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index_1 s))) (simplex_1 s) ∉
        A.obj (Opposite.op { len := dim_1 s })}
  {injective_type₁'_1 :
    ∀ {s t : ι_1},
      { dim := dim_1 s + 1, simplex := simplex_1 s } = { dim := dim_1 t + 1, simplex := simplex_1 t } → s = t}
  {injective_type₂'_1 :
    ∀ {s t : ι_1},
      { dim := dim_1 s,
            simplex :=
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index_1 s))) (simplex_1 s) } =
          { dim := dim_1 t,
            simplex :=
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index_1 t))) (simplex_1 t) } →
        s = t}
  {type₁_ne_type₂'_1 :
    ∀ (s t : ι_1),
      { dim := dim_1 s + 1, simplex := simplex_1 s } ≠
        { dim := dim_1 t,
          simplex :=
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index_1 t))) (simplex_1 t) }}
  {surjective'_1 :
    ∀ (x : A.N),
      ∃ s,
        x.toS = { dim := dim_1 s + 1, simplex := simplex_1 s } ∨
          x.toS =
            { dim := dim_1 s,
              simplex :=
                (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index_1 s)))
                  (simplex_1 s) }},
  { ι := ι, dim := dim, simplex := simplex, index := index, nonDegenerate₁ := nonDegenerate₁,
        nonDegenerate₂ := nonDegenerate₂, notMem₁ := notMem₁, notMem₂ := notMem₂, injective_type₁' := injective_type₁',
        injective_type₂' := injective_type₂', type₁_ne_type₂' := type₁_ne_type₂', surjective' := surjective' } =
      { ι := ι_1, dim := dim_1, simplex := simplex_1, index := index_1, nonDegenerate₁ := nonDegenerate₁_1,
        nonDegenerate₂ := nonDegenerate₂_1, notMem₁ := notMem₁_1, notMem₂ := notMem₂_1,
        injective_type₁' := injective_type₁'_1, injective_type₂' := injective_type₂'_1,
        type₁_ne_type₂' := type₁_ne_type₂'_1, surjective' := surjective'_1 } →
    ι = ι_1 ∧ dim ≍ dim_1 ∧ simplex ≍ simplex_1 ∧ index ≍ index_1