feat: remove Quot.sound axiom from em, provide em_eq without propext

[lyphyser]

This PR changes Classical.em to use a different route that relies on proof irrelevance rather than function extensionality: since proof irrelevance is built-in in Lean, it seems a more appropriate approach.

In addition to removing the axiom dependency, the new proof is much shorter, and provides a version for equalities that only depends on choice, which is now explicitly used in typeDecidableEq, thus removing its dependency on Quot.sound and propext.

[nomeata]

Minimizing use of the standard axiom is an explicit non-goal in the lean4 development.

Although I agree that the new proof looks simpler. Or is that due to heavy golfing? It’s not actually pretty either, just more compact.

Overall, not sure if this contribution pulls its weight.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-05-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-24 16:47:16)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-24 16:47:18)

[lyphyser]

I think it's still simpler with less golfing.

Here is a more verbose version:

theorem em_eq {α : Sort u} (a b : α) : a = b ∨ a ≠ b :=
  let E m := ∃ c, a = m ∧ c ∨ m = b ∧ ¬c
  let hU: E a := ⟨True, .inl ⟨rfl, True.intro⟩⟩
  let hV: E b := ⟨False, .inr ⟨rfl, False.elim⟩⟩

  match choose_spec hU, choose_spec hV with
  | .inr ⟨hab, _⟩, _ => .inl hab
  | _, .inl ⟨hab, _⟩ => .inl hab
  | .inl ⟨_, h⟩, .inr ⟨_, hn⟩ => .inr <| by
    intro hab
    subst a
    exact hn h

theorem em (p : Prop) : p ∨ ¬p :=
  match em_eq p True with
  | .inl h => .inl (of_eq_true h)
  | .inr h => .inr ((mt eq_true) h)

Or even more verbose:

theorem em_eq' {α : Sort u} (a b : α) : a = b ∨ a ≠ b :=
  let hU: ∃ c, a = a ∧ c ∨ a = b ∧ ¬c := ⟨True, .inl ⟨rfl, True.intro⟩⟩
  let hV: ∃ c, a = b ∧ c ∨ b = b ∧ ¬c := ⟨False, .inr ⟨rfl, False.elim⟩⟩

  match choose_spec hU, choose_spec hV with
  | .inr ⟨hab, _⟩, _ => .inl hab
  | _, .inl ⟨hab, _⟩ => .inl hab
  | .inl ⟨_, h⟩, .inr ⟨_, hn⟩ => .inr <| by
    intro hab
    subst a
    exact hn h

EDIT: changed to use a double match, seems more readable

[lyphyser]

Is the "verbose" or "even more verbose" version preferable?

Should I replace the current minimized proof in the pull request with one of those?

[nomeata]

To be honest, I don't think this proof matters enough to justify the discussion, sorry. (Let's use proof irrelevance at the human level :-))

[Kha]

Minimizing use of the standard axiom is an explicit non-goal in the lean4 development.

Indeed. These older proofs will likely be refactored at some later point