You invoke LEM when you can't decide computationally whether a proposition is true or not. If you could decide, you wouldn't invoke it. Admittedly, I exaggerat

You invoke LEM when you can't decide computationally whether a proposition is true or not. If you could decide, you wouldn't invoke it. Admittedly, I exaggerated a bit because my comments were already too long. You can always prove an algorithm correct by using LEM somewhere. It's just nice to have a mathematical universe where "everything is computable" which immediately rules out LEM.