diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 6068d52258..ae1fe42ce2 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -48,6 +48,11 @@ theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide
 
 theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
+@[simp] theorem decide_eq_true {b : Bool} : decide (b = true) = b := by cases b <;> simp
+@[simp] theorem decide_eq_false {b : Bool} : decide (b = false) = !b := by cases b <;> simp
+@[simp] theorem decide_true_eq {b : Bool} : decide (true = b) = b := by cases b <;> simp
+@[simp] theorem decide_false_eq {b : Bool} : decide (false = b) = !b := by cases b <;> simp
+
 /-! ### and -/
 
 @[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide