Correcting my non-expert inaccuracies in this thread: I just learned that Diaconescu's theorem depends on the axiom of choice, which I'd missed even though I'd

Correcting my non-expert inaccuracies in this thread: I just learned that Diaconescu's theorem depends on the axiom of choice, which I'd missed even though I'd glanced at the code for classical.em a few times. So, LEM definitely depends on the axiom of choice in Lean.