linter.unusedSimpArgs misfiring

Stream: mathlib4

[Bhavik Mehta]

The unusedSimpArgs linter sometimes fires in cases where the simp argument is used and necessary. Here's an example:

import Mathlib.Algebra.AddTorsor.Defs
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar

open Pointwise

example {α β : Type*} [AddCommGroup α] [DecidableEq α]
    {S : Finset α} (n : α) {χ : α → β} :
    (∀ k : β, ∃ i ∈ n +ᵥ S, χ i = k) ↔ Set.SurjOn χ (n +ᵥ S) Set.univ := by
  simp [Set.SurjOn, Set.subset_def, ← Finset.coe_vadd_finset]

Is this something we can fix?

[Jovan Gerbscheid]

I think that the simp lemma ← Finset.coe_vadd_finset is actually not used in the final proof term. But removing it still somehow breaks the proof?

[Damiano Testa]

It looks like it suffices to have ← Finset.mem_coe._simp_1, so maybe the lemma brings in some "erased" declaration?

[Damiano Testa]

Maybe, simp generates a list of "extra" lemmas from the list that you give, those lemmas are used in the final proof term, but not the original one, and the linter gets confused.

[Jovan Gerbscheid]

Ah, that's it! The forward lemma is erased from the simp set, so we have to replace it with - Finset.coe_vadd_finset

[Damiano Testa]

So, you really have to "remove it with a -", not just erase it! :lol: