Decidability of the equality of real numbers(DecidableEq)

Stream: mathlib4

[Sehun Kim]

The equality of real numbers is well known to be undecidable
But in the mathlib, there is an instance Real.decidableEq.
As far as I know, if it is not based on the axiom, existence of this instance means that there is a function taking 2 real numbers and computing whether they are same or not.
How could this instance be defined in mathlib?

Following the definition of the Real.decidableEq, it is defined as

noncomputable instance decidableEq (a b : ℝ) : Decidable (a = b) := by infer_instance

And it seems to be defined by

@LinearOrder.decidableEq ℝ Real.linearOrder a b : Decidable (a = b)

And Real.linearOrder is defined by

noncomputable instance linearOrder : LinearOrder ℝ := Lattice.toLinearOrder ℝ

However the function toLinearOrder is defined by

abbrev Lattice.toLinearOrder (α : Type u) [Lattice α] [DecidableEq α]
    [DecidableLE α] [DecidableLT α] [IsTotal α (· ≤ ·)] : LinearOrder α where
  toDecidableLE := ‹_›
  toDecidableEq := ‹_›
  toDecidableLT := ‹_›
  le_total := total_of (· ≤ ·)
  max_def := by exact congr_fun₂ sup_eq_maxDefault
  min_def := by exact congr_fun₂ inf_eq_minDefault

Which requires the DecidableEq α as an instance.
Can someone explain how could Lean accept this definition?

[Aaron Liu]

It uses docs#Classical.propDecidable

[Eric Wieser]

Probably we should reorder those instances to be a bit clearer

[Edward van de Meent]

in particular, it uses it at the definition of Real.toLinearOrder

[Edward van de Meent]

(see here)

[Sehun Kim]

Aha, it uses Classical.propDecidable in somewhere, and it seems to be based on the axiom of excluded middle, if I understood correctly.