From 8131aa5a64b5f3e132a23cdc8ade645d82a1ece9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Feb 2022 13:44:58 -0800 Subject: [PATCH] chore: add simp theorem `heq_eq_eq` --- src/Init/SimpLemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index e686a7ea0c..26ce9215c1 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -148,3 +148,5 @@ theorem dite_congr {s : Decidable b} [Decidable c] @[simp] theorem Nat.beq_to_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp [BEq.beq] @[simp] theorem Nat.not_beq_to_not_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) := by simp [BEq.beq] + +@[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq