fix(data/set/finite): add decidable assumptions (#6264)

Yury's rule of thumb https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/classicalize/near/224871122 says that we should have decidable instances here, because the statements of the lemmas need them (rather than the proofs). I'm making this PR to see if anything breaks.

Author: kbuzzard

src/data/set/finite.lean

@@ -586,33 +586,34 @@ lemma finite.card_to_finset {s : set α} [fintype s] (h : s.finite) :
 by { rw [← finset.card_attach, finset.attach_eq_univ, ← fintype.card], congr' 2, funext,
      rw set.finite.mem_to_finset }
 
-section
-
-local attribute [instance, priority 1] classical.prop_decidable
+section decidable_eq
 
-lemma to_finset_compl {α : Type*} [fintype α] (s : set α) :
-  sᶜ.to_finset = (s.to_finset)ᶜ :=
+lemma to_finset_compl {α : Type*} [fintype α] [decidable_eq α]
+  (s : set α) [fintype (sᶜ : set α)] [fintype s] : sᶜ.to_finset = (s.to_finset)ᶜ :=
 by ext; simp
 
-lemma to_finset_inter {α : Type*} [fintype α] (s t : set α) :
-  (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
+lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)]
+  [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
 by ext; simp
 
-lemma to_finset_union {α : Type*} [fintype α] (s t : set α) :
-  (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
+lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∪ t : set α)]
+  [fintype s] [fintype t] : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
 by ext; simp
 
-lemma to_finset_ne_eq_erase {α : Type*} [fintype α] (a : α) :
-  {x : α | x ≠ a}.to_finset = finset.univ.erase a :=
+lemma to_finset_ne_eq_erase {α : Type*} [decidable_eq α] [fintype α] (a : α)
+  [fintype {x : α | x ≠ a}] : {x : α | x ≠ a}.to_finset = finset.univ.erase a :=
 by ext; simp
 
-lemma card_ne_eq [fintype α] (a : α) :
+lemma card_ne_eq [fintype α] (a : α) [fintype {x : α | x ≠ a}] :
   fintype.card {x : α | x ≠ a} = fintype.card α - 1 :=
-by rw [←to_finset_card, to_finset_ne_eq_erase, finset.card_erase_of_mem (finset.mem_univ _),
-       finset.card_univ, nat.pred_eq_sub_one]
-
+begin
+  haveI := classical.dec_eq α,
+  rw [←to_finset_card, to_finset_ne_eq_erase, finset.card_erase_of_mem (finset.mem_univ _),
+      finset.card_univ, nat.pred_eq_sub_one],
 end
 
+end decidable_eq
+
 section
 
 variables [semilattice_sup α] [nonempty α] {s : set α}