deep recursion error for squeeze_simp

Stream: maths

[Ashvni Narayanan]

Hello, I just completed a proof and was trying to remove the non-terminal simps by using squeeze_simp. I get the following error:

deep recursion was detected at 'replace' (potential solution: increase stack space in your system

The proof is of exp_bernoulli_poly' in the src\number_theory\bernoulli_polynomials.lean file on the bernoulli-polynomials branch. I get the error for the simps on lines 185 and 187 (The proof is a little long).

Any help is appreciated, thank you!

[Eric Wieser]

Try simp?, which is less likely to fail, although more likely to not give you a complete set of lemmas

[Ashvni Narayanan]

Thanks! That worked for the first simp, unfortunately not for the second one (now on line 193). I guess I could try and use rw instead, now that I know the lemmas being used..

[Eric Wieser]

branch#bernoulli-polynomials for others trying to help