∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (leftRetraction : X ⟶ W) (rightRetraction : Y ⟶ X)
  (condition :
    autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
      CategoryTheory.IsSplitEqualizer.condition._autoParam)
  (ι_leftRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction = CategoryTheory.CategoryStruct.id W)
      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam)
  (bottom_rightRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp g rightRetraction = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam)
  (top_rightRetraction :
    autoParam
      (CategoryTheory.CategoryStruct.comp f rightRetraction = CategoryTheory.CategoryStruct.comp leftRetraction ι)
      CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam)
  (leftRetraction_1 : X ⟶ W) (rightRetraction_1 : Y ⟶ X)
  (condition_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
      CategoryTheory.IsSplitEqualizer.condition._autoParam)
  (ι_leftRetraction_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction_1 = CategoryTheory.CategoryStruct.id W)
      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam)
  (bottom_rightRetraction_1 :
    autoParam (CategoryTheory.CategoryStruct.comp g rightRetraction_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam)
  (top_rightRetraction_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp f rightRetraction_1 = CategoryTheory.CategoryStruct.comp leftRetraction_1 ι)
      CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam),
  ({ leftRetraction := leftRetraction, rightRetraction := rightRetraction, condition := condition,
        ι_leftRetraction := ι_leftRetraction, bottom_rightRetraction := bottom_rightRetraction,
        top_rightRetraction := top_rightRetraction } =
      { leftRetraction := leftRetraction_1, rightRetraction := rightRetraction_1, condition := condition_1,
        ι_leftRetraction := ι_leftRetraction_1, bottom_rightRetraction := bottom_rightRetraction_1,
        top_rightRetraction := top_rightRetraction_1 }) =
    (leftRetraction = leftRetraction_1 ∧ rightRetraction = rightRetraction_1)