From 596a547e57550058b050a655db79ac2d0851d0be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Mar 2020 11:17:41 -0700
Subject: [PATCH] feat: add helper theorems

---
 src/Init/Core.lean          | 3 +++
 tests/lean/run/reduce1.lean | 6 ++++++
 2 files changed, 9 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index e0dcee71ed..850a760114 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1739,6 +1739,9 @@ def reduceBool (b : Bool) : Bool := b
   We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
 def reduceNat (n : Nat) : Nat := n
 
+def ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b := h
+def ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b := h
+
 end Lean
 
 /- Classical reasoning support -/
diff --git a/tests/lean/run/reduce1.lean b/tests/lean/run/reduce1.lean
index 06040b608f..1d99a1ede7 100644
--- a/tests/lean/run/reduce1.lean
+++ b/tests/lean/run/reduce1.lean
@@ -15,3 +15,9 @@ def v2 : Bool := 10000000000000000 < 200000000000000000000
 
 theorem tst2 : Lean.reduceBool v2 = true :=
 rfl
+
+theorem tst3 : v1 = 3628800 :=
+Lean.ofReduceNat v1 3628800 rfl
+
+theorem tst4 : v2 = true :=
+Lean.ofReduceBool v2 true rfl