I am wondering how to show that the Lie functor taking Lie groups to Lie algebras is faithful? In particular, I am looking for a constructive proof, since I am working in the context of synthetic differential geometry (and thus restricted to intuitionistic logic).
Sorry if this is an obvious question, but my algebra background isn't that strong, and I mostly taught myself what little Lie theory I know.
There is a reference with a proof given here. It says "the second Lie theorem establishes that this functor is fully faithful". See also here.
For non-connected Lie groups the Lie functor is not faithful, see page $35$ here for "explicit counterexamples".