{M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {R : Type u_10} →
            [inst_2 : Semiring R] →
              [inst_3 : MulSemiringAction M R] →
                {S : Type u_12} →
                  [inst_4 : Semiring S] →
                    [inst_5 : MulSemiringAction N S] →
                      {motive : (R →ₑ+*[φ] S) → Sort u} →
                        (t : R →ₑ+*[φ] S) →
                          ((toDistribMulActionHom : R →ₑ+[φ] S) →
                              (map_one' : toDistribMulActionHom.toFun 1 = 1) →
                                (map_mul' :
                                    ∀ (x y : R),
                                      toDistribMulActionHom.toFun (x * y) =
                                        toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y) →
                                  motive
                                    { toDistribMulActionHom := toDistribMulActionHom, map_one' := map_one',
                                      map_mul' := map_mul' }) →
                            motive t