Commit 2024-05-29 15:57 caa47a8a

fix: extend attributeInstanceIn linter to lint all global attributes declared with in (#13293) Extend the AttributeInstanceIn linter in two ways:

• allow for a list of attributes and flag the ones that are not scoped or local
• also lint any other attribute declared in an attribute in line which is neither scoped nor local (such as ext or simp). This uncovered a global TensorProduct.ext attribute in Mathlib.LinearAlgebra.BilinearForm.TensorProduct. It would have caught #7678 as well. See #13190, especially the final comments by Eric and Mauricio.

theorem what : False := sorry
attribute [simp] what in
#guard true
-- the `simp` attribute on `what` persists
example : False := by simp  -- `simp` finds `what`
theorem who {x y : Nat} : x = y := sorry
attribute [ext] who in
#guard true
-- the `ext` attribute on `who` persists
example {x y : Nat} : x = y := by ext