feat(Data/Set/Basic,Data/Finset/Empty): forall_mem_const for nonempty s (leanprover-community#40745)

Add variants of the `forall_const` `@simp` lemma that localize to a `Nonempty` `Set` or `Finset`.  Here we use the instance form of `Nonempty` (in contrast to the existing `Finset.Nonempty.forall_const`) in order to make `simp` work painlessly.

Co-authored-by: Terence Tao <tao@math.ucla.edu>

Author: teorth

Mathlib/Data/Finset/Empty.lean

@@ -74,6 +74,10 @@ theorem Nonempty.forall_const {s : Finset α} (h : s.Nonempty) {p : Prop} : (∀
   let ⟨x, hx⟩ := h
   ⟨fun h => h x hx, fun h _ _ => h⟩
 
+@[simp]
+theorem forall_mem_const {s : Finset α} [Nonempty s] {p : Prop} : (∀ x ∈ s, p) ↔ p :=
+  (nonempty_coe_sort.mp ‹_›).forall_const
+
 theorem Nonempty.to_subtype {s : Finset α} : s.Nonempty → Nonempty s :=
   nonempty_coe_sort.2
 

Mathlib/Data/Set/Basic.lean

@@ -505,6 +505,14 @@ theorem subset_eq_empty {s t : Set α} (h : t ⊆ s) (e : s = ∅) : t = ∅ :=
 theorem forall_mem_empty {p : α → Prop} : (∀ x ∈ (∅ : Set α), p x) ↔ True :=
   iff_true_intro fun _ => False.elim
 
+theorem Nonempty.forall_const (h : s.Nonempty) {p : Prop} : (∀ x ∈ s, p) ↔ p :=
+  let ⟨x, hx⟩ := h
+  ⟨fun h ↦ h x hx, fun h _ _ ↦ h⟩
+
+@[simp]
+theorem forall_mem_const {p : Prop} [Nonempty s] : (∀ x ∈ s, p) ↔ p :=
+  (nonempty_coe_sort.mp ‹_›).forall_const
+
 instance (α : Type u) : IsEmpty.{u + 1} (↥(∅ : Set α)) :=
   ⟨fun x => x.2⟩