feat: port Data.Fintype.Basic (#1593)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
leanprover-community · Jan 16, 2023 · 8b8d89a · 8b8d89a
1 parent 2cd9351
commit 8b8d89a
Show file tree

Hide file tree

Showing 3 changed files with 1,330 additions and 8 deletions.
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
@@ -2509,6 +2509,10 @@ instance decidableDexistsFinset {p : ∀ a ∈ s, Prop} [_hp : ∀ (a) (h : a
   Multiset.decidableDexistsMultiset
 #align finset.decidable_dexists_finset Finset.decidableDexistsFinset
 
+instance decidableExistsAndFinset {p : α → Prop} [_hp : ∀ (a), Decidable (p a)] :
+    Decidable (∃ a ∈ s, p a) :=
+  decidable_of_iff (∃ (a : _)(_ : a ∈ s), p a) (by simp)
+
 end DecidablePiExists
 
 /-! ### filter -/