feat: add warning when applying global attribute using in (#13223)

This PR adds a warning preventing a user from applying global attribute
using `... in ...`, e.g.
```lean4
theorem a : True := trivial
attribute [simp] a in
def b : True := a
```

src/Lean/Linter.lean

@@ -18,3 +18,4 @@ public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
+public import Lean.Linter.GlobalAttributeIn

src/Lean/Linter/GlobalAttributeIn.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Linter.Basic
+
+
+namespace Lean.Linter
+open Elab.Command
+
+private structure TopDownSkipQuot where
+  stx : Syntax
+
+def topDownSkipQuot (stx : Syntax) : TopDownSkipQuot := ⟨stx⟩
+
+partial instance [Monad m] : ForIn m TopDownSkipQuot Syntax where
+  forIn := fun ⟨stx⟩ init f => do
+    let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
+      if stx.isQuot then return ForInStep.yield b
+      match (← f stx b) with
+      | ForInStep.yield b' =>
+        let mut b := b'
+        if let Syntax.node _ _ args := stx then
+          for arg in args do
+            match (← loop arg b) with
+            | ForInStep.yield b' => b := b'
+            | ForInStep.done b'  => return ForInStep.done b'
+        return ForInStep.yield b
+      | ForInStep.done b => return ForInStep.done b
+    match (← @loop stx init ⟨init⟩) with
+    | ForInStep.yield b => return b
+    | ForInStep.done b  => return b
+
+def getGlobalAttributesIn? : Syntax → Option (Ident × Array (TSyntax `attr))
+  | `(attribute [$x,*] $id in $_) =>
+    let xs := x.getElems.filterMap fun a => match a.raw with
+      | `(Parser.Command.eraseAttr| -$_) => none
+      | `(Parser.Term.attrInstance| local $_attr:attr) => none
+      | `(Parser.Term.attrInstance| scoped $_attr:attr) => none
+      | `(attr| $a) => some a
+    (id, xs)
+  | _ => default
+
+def globalAttributeIn : Linter where run := withSetOptionIn fun stx => do
+  for s in topDownSkipQuot stx do
+    if let some (id, nonScopedNorLocal) := getGlobalAttributesIn? s then
+      for attr in nonScopedNorLocal do
+        logErrorAt attr
+          m!"Despite the `in`, the attribute {attr} is added globally to {id}\n\
+          please remove the `in` or make this a `local {attr}`"
+
+builtin_initialize addLinter globalAttributeIn
+
+end Lean.Linter

tests/elab/1829.lean

@@ -1,4 +1,4 @@
-attribute [simp] eq_iff_true_of_subsingleton in
+attribute [simp] eq_iff_true_of_subsingleton
 example : True := trivial
 
 structure Func' (α : Sort _) (β : Sort _) :=

tests/elab/globalAttributesIn.lean

@@ -0,0 +1,56 @@
+def t : True := by simp
+
+/--
+error: Despite the `in`, the attribute irreducible is added globally to t
+please remove the `in` or make this a `local irreducible`
+-/
+#guard_msgs in
+attribute [local simp, irreducible] t in
+example : True := t
+
+/--
+error: Despite the `in`, the attribute simp is added globally to t
+please remove the `in` or make this a `local simp`
+-/
+#guard_msgs in
+attribute [simp] t in
+example : True := t
+
+def t' : True := by simp
+
+/--
+error: Despite the `in`, the attribute simp is added globally to t'
+please remove the `in` or make this a `local simp`
+---
+error: Despite the `in`, the attribute irreducible is added globally to t'
+please remove the `in` or make this a `local irreducible`
+-/
+#guard_msgs in
+attribute [simp, irreducible] t' in
+example : True := t'
+
+attribute [local simp] t in
+example : True := t
+
+section
+/--
+error: Despite the `in`, the attribute simp is added globally to t
+please remove the `in` or make this a `local simp`
+-/
+#guard_msgs in
+attribute [simp] t in
+example : True := t
+end
+
+/--
+error: Despite the `in`, the attribute simp is added globally to t
+please remove the `in` or make this a `local simp`
+---
+error: Despite the `in`, the attribute simp is added globally to t'
+please remove the `in` or make this a `local simp`
+-/
+#guard_msgs in
+attribute [simp] t in
+set_option trace.Meta.Tactic true in
+attribute [simp] t' in
+example : True := t

tests/elab/rewrite.lean

@@ -32,7 +32,7 @@ example (h : f (f 1) = 0) : f (g 1) = 0 := by
 example (h : f (f 1) = 0) : f (g 1) = 0 := by
   rw (config := {transparency := .default}) [h] -- This is just `erw`.
 
-attribute [reducible] f in
+attribute [reducible] f
 example : f 1 = f 2 := by
   rw [] -- Empty rewrite closes the goal via `rfl`
 example : f 1 = f 2 := by

tests/elab/solve_by_elim.lean

@@ -74,7 +74,7 @@ example (P₁ P₂ : α → Prop) (f : ∀ (a: α), P₁ a → P₂ a → β)
   fail_if_success solve_by_elim (config := .noBackTracking)
   solve_by_elim
 
-attribute [symm] Eq.symm in
+attribute [symm] Eq.symm
 example {α : Type} {a b : α → Prop} (h₀ : b = a) (y : α) : a y = b y := by
   fail_if_success solve_by_elim (config := {symm := false})
   solve_by_elim

tests/elab/test_simp_reducible_class.lean

@@ -29,13 +29,13 @@ example : (instX a).x = (instX b).x := by simp
 -- isDefEqProj bumps to .instances via withInstanceConfig.
 -- With backward.whnf.reducibleClassField = true: tryHeuristic in isDefEqDelta applies the
 -- argument-comparison heuristic, and isDefEqArgs bumps to .instances for instance-implicit params.
-set_option allowUnsafeReducibility true in
-attribute [reducible] X.x in
+set_option allowUnsafeReducibility true
+attribute [reducible] X.x
 example : (instX a).x = (instX b).x := by simp
 
 -- Test 2b: same as Test 2 with backward.whnf.reducibleClassField explicitly enabled
-set_option allowUnsafeReducibility true in
-attribute [reducible] X.x in
+set_option allowUnsafeReducibility true
+attribute [reducible] X.x
 set_option backward.whnf.reducibleClassField true in
 example : (instX a).x = (instX b).x := by simp