∀ {D : Type u_5} {inst : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6} {inst_1 : AddCommMonoid M}
  {inst_2 : CategoryTheory.HasShift D M}
  {toTwistShiftData :
    CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
      (M × M)}
  {z_zero₁ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (0, m₁) (0, m₂) = 1) CategoryTheory.CommShift₂Setup.z_zero₁._autoParam}
  {z_zero₂ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (m₁, 0) (m₂, 0) = 1) CategoryTheory.CommShift₂Setup.z_zero₂._autoParam}
  {ε : M → M → (CategoryTheory.CatCenter D)ˣ}
  {hε :
    autoParam (∀ (m n : M), ε m n = (toTwistShiftData.z (0, n) (m, 0))⁻¹ * toTwistShiftData.z (m, 0) (0, n))
      CategoryTheory.CommShift₂Setup.hε._autoParam}
  {toTwistShiftData_1 :
    CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
      (M × M)}
  {z_zero₁_1 :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData_1.z (0, m₁) (0, m₂) = 1)
      CategoryTheory.CommShift₂Setup.z_zero₁._autoParam}
  {z_zero₂_1 :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData_1.z (m₁, 0) (m₂, 0) = 1)
      CategoryTheory.CommShift₂Setup.z_zero₂._autoParam}
  {ε_1 : M → M → (CategoryTheory.CatCenter D)ˣ}
  {hε_1 :
    autoParam (∀ (m n : M), ε_1 m n = (toTwistShiftData_1.z (0, n) (m, 0))⁻¹ * toTwistShiftData_1.z (m, 0) (0, n))
      CategoryTheory.CommShift₂Setup.hε._autoParam},
  { toTwistShiftData := toTwistShiftData, z_zero₁ := z_zero₁, z_zero₂ := z_zero₂, ε := ε, hε := hε } =
      { toTwistShiftData := toTwistShiftData_1, z_zero₁ := z_zero₁_1, z_zero₂ := z_zero₂_1, ε := ε_1, hε := hε_1 } →
    toTwistShiftData = toTwistShiftData_1 ∧ ε = ε_1