refactor: remove funext dependency from Classical.em, drop Quot.sound

[tchaumeny]

This PR removes the usage of funext in the proof of excluded-middle (Diaconescu's theorem). As a result, the dependency on the axiom Quot.sound disappears from em.

This small refactoring is inspired by this MO question by Jean Abou Samra.

It also makes the proof substantially simpler while keeping the original structure.

Before

#print axioms em
'Classical.em' depends on axioms: [propext, choice, Quot.sound]

After

#print axioms em
'Classical.em' depends on axioms: [propext, choice]

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 52edefc40e92425b6bb2671c01420b7f76fb6caf --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-16 18:49:29)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 52edefc40e92425b6bb2671c01420b7f76fb6caf --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force reference manual CI using the force-manual-ci label. (2026-07-16 18:49:31)

[SnirBroshi]

Cool!

[TwoFX]

As discussed, reducing axioms beyond the three standard axioms is not a goal of the Lean standard library, and neither is the proofs being useful pedagogically. So I'm closing this PR.