PR 4715

Stream: new members

[Damiano Testa]

Dear All,

in #4175 #4715 Lean gives a linting error in finset/basic.lean. I do not think that this is a result of the changes that I made, but I am not sure. Anyway, simply changing β to γ in the statement of the lemma below is enough to fix the lint error, at least according to the #lint at the bottom of the current file. Is it ok if I simply do this, or should I perform a different change?

Thank you!

lemma nonempty.map (h : s.nonempty) (f : α ↪ β) : (s.map f).nonempty :=
let ⟨a, ha⟩ := h in ⟨f a, (mem_map' f).mpr ha⟩

[Damiano Testa]

(For added context: the lint error is

/- Checking 519 declarations (plus 152 automatically generated ones) in the current file -/

/- The `unused_arguments` linter reports: -/
/- UNUSED ARGUMENTS: -/
#print finset.nonempty.map /- argument 3: [_inst_1 : decidable_eq β] -/

/- The `decidable_classical` linter reports: -/
/- USES OF `decidable` SHOULD BE REPLACED WITH `classical` IN THE PROOF.: -/
#print finset.nonempty.map /- The following `decidable` hypotheses should be replaced with
                      `classical` in the proof. argument 3: [_inst_1 : decidable_eq β] -/

and \beta is assumed to have decidable_eq, while \gamma is not.)

[Ruben Van de Velde]

Is that the right PR? #4175 seems to have been merged already

[Damiano Testa]

Sorry, my mistake! #4715!

[Damiano Testa]

I will change it elsewhere as well! Thanks!

[Yury G. Kudryashov]

There is a [decidable_eq] assumption in variables in this section. While finset.image needs decidable_eq on the codomain, finset.map doesn't need it. I suggest that you move your lemma to the section with lemmas about finset.map or choose a type variable without [decidable_eq] assumption.

[Damiano Testa]

Yury G. Kudryashov said:

There is a [decidable_eq] assumption in variables in this section. While finset.image needs decidable_eq on the codomain, finset.map doesn't need it. I suggest that you move your lemma to the section with lemmas about finset.map or choose a type variable without [decidable_eq] assumption.

I moved the lemma (with the target type called \beta) at the end of the previous section (map). Everything seems to still work and lint gives no errors. Is this preferable to renaming \beta to \gamma ?

[Ruben Van de Velde]

It sounds like a good idea in general to keep everything about map together

[Damiano Testa]

Ok, I will move the lemma nonempty.map to the previous section then and push again the change. Hopefully, the PR will pass all the tests!

Thank you very much for your help!