decidable_classical linter complaint

Stream: general

[Paul van Wamelen]

I have a theorem that I would like to add to the ring_theory/unique_factorization_domain.lean file, but the decidable_classical linter complains with

The following `decidable` hypotheses should be replaced with
                      `classical` in the proof. argument 4: [dec : decidable_eq (associates α)]

There are many other theorems that have the exact same hypothesis, but without a complaint. Why is that? Also, how do I fix this case?

[Mario Carneiro]

As long as the hypothesis is referenced directly in the statement (usually invisibly because it is a type class argument), the linter will not complain

[Mario Carneiro]

You can fix it by removing the decidable_eq instance from the theorem, and then starting the proof with classical,

[Mario Carneiro]

I see in ring_theory/unique_factorization_domain.lean that the dec hypothesis is added on L305, included in the definition factors (meaning that all theorems directly about factors will need this assumption), and later explicitly omitted in theorems eq_of_prod_eq_prod and prod_le, by putting omit dec before the theorem and include dec after. You can do that for your theorem as well

[Paul van Wamelen]

Thanks Mario, I'll try that!