Modern proof assistants make it possible to verify proofs and programs, but also to perform computations, and sometimes to find proofs automatically. By using various tools and techniques to solve well-defined classes of goals, infer appropriate data, or perform high-level reasoning steps, I will show how to obtain robust and elegant proof scripts in several application domains: analysis, relation algebra, and category theory.