∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op (SimplexCategory.mk 0))} {f g fg : X.PtSimplex n x} {i : Fin n}
  (map : SSet.stdSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ X)
  (δ_castSucc_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam)
  (δ_succ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam)
  (δ_succ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam)
  (δ_map_of_lt :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam)
  (map_1 : SSet.stdSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ X)
  (δ_castSucc_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map_1 = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam)
  (δ_succ_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map_1 = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam)
  (δ_succ_succ_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map_1 = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam)
  (δ_map_of_lt_1 :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt_1 :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam),
  ({ map := map, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map, δ_succ_castSucc_map := δ_succ_castSucc_map,
        δ_succ_succ_map := δ_succ_succ_map, δ_map_of_lt := δ_map_of_lt, δ_map_of_gt := δ_map_of_gt } =
      { map := map_1, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map_1,
        δ_succ_castSucc_map := δ_succ_castSucc_map_1, δ_succ_succ_map := δ_succ_succ_map_1,
        δ_map_of_lt := δ_map_of_lt_1, δ_map_of_gt := δ_map_of_gt_1 }) =
    (map = map_1)