feat: lake: getLakeSharedDynlib (#14364)

This PR adds `getLakeSharedDynlib` to the Lake API. It is a simple
monadic convenience function that retrieves `LakeInstall.sharedDynlib`
for the detected Lake installation.

Author: tydeu

src/lake/Lake/Config/Monad.lean

@@ -364,4 +364,8 @@ Returns the path of the primary core shared library
 @[inline] public def getLake : m FilePath :=
   (·.lake) <$> getLakeInstall
 
+/-- Get the Lake shared library (e.g., {lit}`libLake_shared`) in the detected Lake installation. -/
+@[inline] public def getLakeSharedDynlib : m Dynlib :=
+  (·.sharedDynlib) <$> getLakeInstall
+
 end