{α : Type u} →
  {P : Sort u_1} →
    {toNonUnitalSemiring : NonUnitalSemiring α} →
      {toOne : One α} →
        {one_mul : ∀ (a : α), 1 * a = a} →
          {mul_one : ∀ (a : α), a * 1 = a} →
            {toNatCast : NatCast α} →
              {natCast_zero : autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam} →
                {natCast_succ : autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam} →
                  {npow : ℕ → α → α} →
                    {npow_zero : autoParam (∀ (x : α), npow 0 x = 1) Monoid.npow_zero._autoParam} →
                      {npow_succ :
                          autoParam (∀ (n : ℕ) (x : α), npow (n + 1) x = npow n x * x) Monoid.npow_succ._autoParam} →
                        {toNonUnitalSemiring' : NonUnitalSemiring α} →
                          {toOne' : One α} →
                            {one_mul' : ∀ (a : α), 1 * a = a} →
                              {mul_one' : ∀ (a : α), a * 1 = a} →
                                {toNatCast' : NatCast α} →
                                  {natCast_zero' : autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam} →
                                    {natCast_succ' :
                                        autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1)
                                          AddMonoidWithOne.natCast_succ._autoParam} →
                                      {npow' : ℕ → α → α} →
                                        {npow_zero' :
                                            autoParam (∀ (x : α), npow' 0 x = 1) Monoid.npow_zero._autoParam} →
                                          {npow_succ' :
                                              autoParam (∀ (n : ℕ) (x : α), npow' (n + 1) x = npow' n x * x)
                                                Monoid.npow_succ._autoParam} →
                                            { toNonUnitalSemiring := toNonUnitalSemiring, toOne := toOne,
                                                  one_mul := one_mul, mul_one := mul_one, toNatCast := toNatCast,
                                                  natCast_zero := natCast_zero, natCast_succ := natCast_succ,
                                                  npow := npow, npow_zero := npow_zero, npow_succ := npow_succ } =
                                                { toNonUnitalSemiring := toNonUnitalSemiring', toOne := toOne',
                                                  one_mul := one_mul', mul_one := mul_one', toNatCast := toNatCast',
                                                  natCast_zero := natCast_zero', natCast_succ := natCast_succ',
                                                  npow := npow', npow_zero := npow_zero', npow_succ := npow_succ' } →
                                              (toNonUnitalSemiring ≍ toNonUnitalSemiring' →
                                                  toOne ≍ toOne' → toNatCast ≍ toNatCast' → npow ≍ npow' → P) →
                                                P