Bug Help?

Stream: general

[Taylor Belcher]

Hello -- I have a file that will work when placed in one Lean Project but not another and I cannot figure out why. simp_not_working.png simp_working.png

[Jireh Loreaux]

Are you working from the same version of mathlib? Also, you can see which lemmas were applied in the succeeding version by using squeeze_simp

[Mario Carneiro]

Also post text not images (#backticks, #mwe)