Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level integrals, like $\int_0^1xe^x\,dx$, and not anything excessively crazy.
Of course, if our goal is merely to have a proof of a statement of the form $\int_a^bf(x)\,dx=c$ for some known $c$, then proving this in Lean should be possible by finding a function $F(x)$, check $F'(x)=f(x)$, evaluating $F(b)-F(a)$ and appealing to FTC. But this is an approach which is very backwards compared to how this is done by hand (which, at least somewhat implicitly, involves finding such an $F$).
My question is, does Lean have any tools which would let you perform such "by hand" calculations within your code? At the very least it would require support for integration by parts and integration by substitution, and I'm not sure those are in mathlib. Ideally I would also imagine some kind of environment like the calc mode.
If not in Lean, are there similar tools available in other proof assistants?
Just to clarify, I do not mean automated computation of integrals like in CAS. I just mean tools which would let you painlessly perform IBP and substitutions (and perhaps other operations) on given integrals to simplify them.