From 872a885104e02f1e1ae7084f52a80d457f5c0724 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 11 Sep 2024 18:23:43 +1000 Subject: [PATCH] chore: remove @[simp] from forall_const --- src/Init/PropLemmas.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index aa8946f6a4e5..ab047a98f8ae 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -303,9 +303,13 @@ theorem exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x := @[simp] theorem exists_false : ¬(∃ _a : α, False) := fun ⟨_, h⟩ => h -@[simp] theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b := +-- This is not a good simp lemma, as it applies to any arrow, and generates a `Nonempty` side goal. +theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b := ⟨i.elim, fun hb _ => hb⟩ +@[simp] theorem not_forall_of_nonempty [Nonempty β] : ((α → β) → False) ↔ False := by + simp [forall_const] + theorem Exists.nonempty : (∃ x, p x) → Nonempty α | ⟨x, _⟩ => ⟨x⟩ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x