-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.mk.injEq : ∀ {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)