∀ (M : Type u_1) (N : Type u_2) [inst : Monoid M] [inst_1 : Monoid N] (x : { _inst // IsScalarTower M N N }),
  ⟨MulAction.compHom N
        (match x with
        | ⟨val, property⟩ => MonoidHom.smulOneHom),
      ⋯⟩ =
    x