Refactoring with unused-fintype linter

Stream: mathlib4

[Snir Broshi]

This is about a graph-theory PR but it's a general Mathlib question. btw I love the unused-fintype linter in general, but I'm not sure what to do here.

#33501 changes a def (docs#SimpleGraph.degree) from s.toFinset.card which has to assume [Fintype s], to s.ncard, to avoid the Fintype assumption (s is a Set btw).
This triggers the following:

• Changing a def means changing a bunch of places that defeq-abused
• The unusedFintypeInType now triggers on many theorems, and requires changing [Fintype s] to [Finite s]. I use omit instead of moving theorems between sections to make the diff bearable.
• Now using Finite on sets is discouraged, and I have to change all the [Finite s] to (h : s.Finite) which triggers a ton of new places that break.

I can do the work, but I worry that stuffing it all in a single PR makes it unlikely to be merged.
The question is: can we do something to allow such refactors to chunk their changes, to help contributors/reviewers/maintainers?

I thought about just adding a bunch of set_option linter.unusedFintypeInType false, is that reasonable given that I'm going to fix them in future PRs? (and hopefully soon)
Or can we change the policy to allow [Finite s] as a transient state?

cc @Yaël Dillies

[Johan Commelin]

I think that indeed disabling linters at certain points is a good strategy.
Even if that bumps up the tech debt counters, you aren't adding tech debt, but exposing it.