diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 5f1c4663029c..851a5ec81926 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -32,39 +32,16 @@ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :
 theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
   (indefiniteDescription p h).property
 
-/-- **Diaconescu's theorem**: excluded middle from choice, Function extensionality and propositional extensionality. -/
+/-- **Diaconescu's theorem** for equalities: excluded middle from choice using proof irrelevance. -/
+theorem em_eq {α : Sort u} (a b : α) : a = b ∨ a ≠ b :=
+  let E m := ∃ c, a = m ∧ c ∨ m = b ∧ ¬c
+  (.inl ·.1) |> (choose_spec (⟨True, .inl ⟨rfl, ⟨⟩⟩⟩ : E a)).elim fun h =>
+    (choose_spec (⟨False, .inr ⟨rfl, id⟩⟩ : E b)).imp (·.1) fun
+      | hn, rfl => hn.2 h.2
+
+/-- **Diaconescu's theorem**: excluded middle from choice and propositional extensionality, using proof irrelevance. -/
 theorem em (p : Prop) : p ∨ ¬p :=
-  let U (x : Prop) : Prop := x = True ∨ p
-  let V (x : Prop) : Prop := x = False ∨ p
-  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
-  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
-  let u : Prop := choose exU
-  let v : Prop := choose exV
-  have u_def : U u := choose_spec exU
-  have v_def : V v := choose_spec exV
-  have not_uv_or_p : u ≠ v ∨ p :=
-    match u_def, v_def with
-    | Or.inr h, _ => Or.inr h
-    | _, Or.inr h => Or.inr h
-    | Or.inl hut, Or.inl hvf =>
-      have hne : u ≠ v := by simp [hvf, hut]
-      Or.inl hne
-  have p_implies_uv : p → u = v :=
-    fun hp =>
-    have hpred : U = V :=
-      funext fun x =>
-        have hl : (x = True ∨ p) → (x = False ∨ p) :=
-          fun _ => Or.inr hp
-        have hr : (x = False ∨ p) → (x = True ∨ p) :=
-          fun _ => Or.inr hp
-        show (x = True ∨ p) = (x = False ∨ p) from
-          propext (Iff.intro hl hr)
-    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
-      rw [hpred]; intros; rfl
-    show u = v from h₀ _ _
-  match not_uv_or_p with
-  | Or.inl hne => Or.inr (mt p_implies_uv hne)
-  | Or.inr h   => Or.inl h
+  (em_eq p True).imp of_eq_true (mt eq_true)
 
 theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
   | ⟨x⟩ => ⟨x, trivial⟩
@@ -90,7 +67,9 @@ noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
 instance (a : Prop) : Nonempty (Decidable a) := ⟨propDecidable a⟩
 
 noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
-  fun _ _ => inferInstance
+  (choice <| match em_eq · · with
+    | .inl h => ⟨isTrue h⟩
+    | .inr h => ⟨isFalse h⟩)
 
 noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
   match (propDecidable (Nonempty α)) with