Isabelle semi-automatic theorem prover tries to help with 2 if you use sledgehammer strategy and print out the simplified proof with isar_proofs argument, which you can more easily read and reintegrate into the main document if needed.

You can help its heuristics by providing it a set of potential proof facts explicitly.

The libraries available for it are already quite huge... sometimes in a few encodings as well. (valued, typed, functional etc.)

https://www.isa-afp.org/