diff --git a/library/init/data/bool/lemmas.lean b/library/init/data/bool/lemmas.lean
index c5d85710b8..80c73aba52 100644
--- a/library/init/data/bool/lemmas.lean
+++ b/library/init/data/bool/lemmas.lean
@@ -101,7 +101,7 @@ show (ff = tt) = false, by simp
 @[simp] lemma coe_tt : ↑tt = true :=
 show (tt = tt) = true, by simp
 
-theorem to_bool_iff (p : Prop) [d : decidable p] : to_bool p ↔ p :=
+@[simp] theorem to_bool_iff (p : Prop) [d : decidable p] : (to_bool p = tt) ↔ p :=
 match d with
 | is_true hp := ⟨λh, hp, λ_, rfl⟩
 | is_false hnp := ⟨λh, bool.no_confusion h, λhp, absurd hp hnp⟩
@@ -117,7 +117,7 @@ theorem bool_iff_false {b : bool} : ¬ b ↔ b = ff := by cases b; exact dec_tri
 
 theorem bool_eq_false {b : bool} : ¬ b → b = ff := bool_iff_false.1
 
-theorem to_bool_ff_iff (p : Prop) [decidable p] : to_bool p = ff ↔ ¬p :=
+@[simp] theorem to_bool_ff_iff (p : Prop) [decidable p] : to_bool p = ff ↔ ¬p :=
 bool_iff_false.symm.trans (not_congr (to_bool_iff _))
 
 theorem to_bool_ff {p : Prop} [decidable p] : ¬p → to_bool p = ff := (to_bool_ff_iff p).2
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 1a0aa5d9d4..678077b3db 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -589,6 +589,12 @@ decidable.cases_on h (λ h₁, bool.ff) (λ h₂, bool.tt)
 
 export decidable (is_true is_false to_bool)
 
+@[simp] lemma to_bool_true_eq_tt (h : decidable true) : @to_bool true h = tt :=
+decidable.cases_on h (λ h, false.elim (iff.mp not_true h)) (λ _, rfl)
+
+@[simp] lemma to_bool_false_eq_ff (h : decidable false) : @to_bool false h = ff :=
+decidable.cases_on h (λ h, rfl) (λ h, false.elim h)
+
 instance decidable.true : decidable true :=
 is_true trivial