diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index d05aea8f2a..16db2812f3 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -80,6 +80,8 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid
 noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
   default := inferInstance
 
+instance (a : Prop) : Nonempty (Decidable a) := ⟨propDecidable a⟩
+
 noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
   fun _ _ => inferInstance
 
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index aa8946f6a4..697eb73e3e 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -352,10 +352,10 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
 @[simp] theorem exists_or_eq_left' (y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x := ⟨y, .inl rfl⟩
 @[simp] theorem exists_or_eq_right' (y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x := ⟨y, .inr rfl⟩
 
-@[simp] theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p :=
+theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p :=
   ⟨fun ⟨a, h⟩ => ⟨⟨a⟩, h⟩, fun ⟨⟨a⟩, h⟩ => ⟨a, h⟩⟩
 
-theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
+@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
   ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩
 
 @[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩