From bae7d582357bcb58906bd4acd7f3b56ae544954e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 12 Sep 2024 14:52:53 +1000 Subject: [PATCH] chore: restrict exists_prop' to Type --- src/Init/PropLemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index aa8946f6a4e5..99aed1fd8b69 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 := +@[simp] theorem exists_prop' {α : Type _} {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 (p q : Prop): (∃ _h : p, q) ↔ p ∧ q := ⟨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⟩