upstreamableDecl linter bug

Stream: mathlib4

[Kim Morrison]

Try adding
import Mathlib.Tactic.Linter.UpstreamableLinter and set_option linter.upstreamableDecl true in Mathlib.Algebra.Group.Equiv.Basic.

This incorrectly reports that

protected theorem congr_arg {f : MulEquiv M N} {x x' : M} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

can be moved up to Mathlib.Data.FunLike.Basic, despite MulEquiv only being defined in the current file.

(@Damiano Testa, @Anne Baanen)

[Damiano Testa]

I'll try to take a look tomorrow: my suspect is that MulEquiv is a structure and not a def and that may be confusing the linter. But I'm not at a computer now.

[Anne Baanen]

My dbg_trace agrees with @Damiano Testa: all the definitions in the current file this depends on are structures and instances, not defs.

[Anne Baanen]

Still, shouldn't this theorem transitively depend on an EquivLike instance, whose type is not available in Funlike.Basic?

[Anne Baanen]

The list of directly-depended on decls fir congr_arg is:

deps: #[Lean.Parser.Command.declId,
 Lean.Parser.Term.attributes,
 congrArg,
 Lean.Parser.Command.theorem,
 Lean.Parser.Term.typeSpec,
 Eq.rec,
 «term_=_»,
 Lean.Parser.Command.declSig,
 Lean.Parser.Term.implicitBinder,
 Lean.Parser.Term.attrInstance,
 Lean.Parser.Term.attrKind,
 Lean.Parser.Command.declaration,
 Lean.Parser.Termination.suffix,
 congr_arg,
 Lean.Parser.Term.app,
 MulEquiv,
 Eq.refl,
 Lean.Parser.Command.declValSimple,
 Lean.Parser.Command.protected,
 Lean.Parser.Command.declModifiers,
 Lean.Parser.Term.arrow,
 toAdditiveRest,
 Eq,
 to_additive,
 rfl,
 DFunLike.congr_arg]

[Damiano Testa]

It would probably be useful to expand the API a bit to have that trace split into defs theorems,... and the syntax, tactics (not exactly sure how granular to make it).

[Damiano Testa]

I may have time for this tomorrow, though I'm not sure.

[Anne Baanen]

Actually, picking some other declarations in that file at random, it seems like quite a few instances are missing. For example docs#MulEquivClass.map_mul doesn't report any instances except instHMul...

[Anne Baanen]

Fix for the originally reported issue, where declarations depending on structures like MulEquiv shouldn't get warnings: #19360.