diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 9438d4724970..26e987c0a985 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1362,6 +1362,9 @@ theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b := Iff.comm.trans (iff_fa
 theorem of_iff_true    (h : a ↔ True) : a := h.mpr trivial
 theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h trivial
 
+theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
+  iff_true_intro (Subsingleton.elim ..)
+
 theorem not_of_iff_false : (p ↔ False) → ¬p := Iff.mp
 theorem iff_false_intro (h : ¬a) : a ↔ False := iff_of_false h id
 
diff --git a/tests/lean/discrTreeIota.lean b/tests/lean/discrTreeIota.lean
index ad09962355e2..ff8c79bbdb66 100644
--- a/tests/lean/discrTreeIota.lean
+++ b/tests/lean/discrTreeIota.lean
@@ -1,9 +1,6 @@
 @[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
     Quot.liftOn (Quot.mk r a) f h = f a := rfl
 
-theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
-  iff_true _ ▸ Subsingleton.elim ..
-
 section attribute [simp] eq_iff_true_of_subsingleton end
 
 @[simp] theorem PUnit.default_eq_unit : (default : PUnit) = PUnit.unit := rfl
diff --git a/tests/lean/run/1829.lean b/tests/lean/run/1829.lean
index 8a53e8a04467..bf7efa175b8d 100644
--- a/tests/lean/run/1829.lean
+++ b/tests/lean/run/1829.lean
@@ -1,6 +1,3 @@
-theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
-  ⟨fun _ => ⟨⟩, fun _ => (Subsingleton.elim ..)⟩
-
 attribute [simp] eq_iff_true_of_subsingleton in
 example : True := trivial