u sub in lean?

Stream: maths

[Mason McBride]

let's say I was solving an integral in lean in an itp type of way, is it possible to set 'u' to valid terms and watch the integral update?

[Eric Wieser]

You might be interested in the lemmas here: https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/interval_integral.html#integration-by-substitution--change-of-variables

[Mason McBride]

this is interesting thanks