From 7bb9638ea6252d16b78f8f8b04d91b7c173abbf7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Mar 2020 06:35:00 -0700
Subject: [PATCH] feat: helper lemmas for equation compiler

---
 src/Init/Core.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 4f15da8ad7..e113f1e2e0 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1019,6 +1019,16 @@ match h with
 | (isTrue hc)   => absurd hc hnc
 | (isFalse hnc) => rfl
 
+theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
+match h with
+| (isTrue  hc)  => rfl
+| (isFalse hnc) => absurd hc hnc
+
+theorem difNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
+match h with
+| (isTrue hc)   => absurd hc hnc
+| (isFalse hnc) => rfl
+
 -- Remark: dite and ite are "defally equal" when we ignore the proofs.
 theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
 match h with