## Stream: new members

### Topic: PR 4715

#### Damiano Testa (Oct 25 2020 at 09:48):

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 (Oct 25 2020 at 09:52):

(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 (Oct 25 2020 at 09:53):

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

#### Damiano Testa (Oct 25 2020 at 09:53):

Sorry, my mistake! #4715!

#### Damiano Testa (Oct 25 2020 at 09:53):

I will change it elsewhere as well! Thanks!

#### Yury G. Kudryashov (Oct 25 2020 at 09:58):

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 (Oct 25 2020 at 10:01):

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 (Oct 25 2020 at 10:06):

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

#### Damiano Testa (Oct 25 2020 at 10:07):

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!

Last updated: May 16 2021 at 05:21 UTC