Create library note explaining seemingly redundant fintype and decidable arguments.

[kmill]

Although fintype and decidable are (sub)singletons, since different instances are not definitionally equal, it's useful to have instance arguments that are seemingly redundant. For example:

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

The [fintype (s ∩ t : set α)] instance is inferrable from either of the other two, but to make sure this lemma is maximally applicable each fintype instance should be its own parameter.

This pattern should be documented somewhere, possibly as a library note.

[vihdzp]

Surely it's still a good idea to have the stronger variants separately as lemmas rather than instances, right?