What contributes to a function slowing down in Lean?

Stream: new members

[Vivek Rajesh Joshi]

I have this function to calculate the row echelon form of a matrix, which takes about 15-20 seconds to run for a 3x3. Another function that runs the back substitution phase of gaussian elimination for a matrix does so almost instantly. However, if I make a new function that applies the back substitution function to the output of the row echelon function (essentially giving the row-reduced echelon form of the matrix), it takes 6 minutes to process a 3x3 matrix. What can I do to improve this?
Here's the file, if anyone wants to have a look: https://github.com/vivek-rj/gauss_elim1/blob/master/GaussElim/ge_test2vec.lean

[Chris Bailey]

This thread may be of interest.

[Michael Rothgang]

One take-away form that thread: running your code in #eval can be very slow: compiling your code can speed it up a lot. In other words: that thread's advice definitely looks applicable here. If it's still slow after that, that's much more interesting.