test: expand tests/lean/issue2981.lean a bit (#3007)

tests/lean/issue2981.lean

@@ -25,3 +25,37 @@ def rec : Nat → Nat → Nat
 decreasing_by trace "Tactic is run (ideally only twice)"; decreasing_tactic
 
 end TestingGuessLex
+
+
+namespace Subcontext
+
+set_option linter.unusedVariables false
+
+-- Now with a duplication into another context
+-- We thread through `x` so that we can make the context mention something
+-- that appears in the goal, else `mvarId.cleanup` will remove it
+def dup2 (x : Nat) (a : Nat) (b : x ≠ x → Nat := fun h => a) := a
+
+namespace TestingFix
+def rec : Nat → Nat
+ | 0 => 1
+ | n+1 => dup2 n (rec n)
+decreasing_by
+  trace "Tactic is run (ideally only once, in most general context)"
+  trace_state
+  decreasing_tactic
+
+end TestingFix
+
+namespace TestingGuessLex
+
+-- GuessLex should run the tactic an extra time, that is expected
+def rec : Nat → Nat → Nat
+ | 0, _m => 1
+ | n+1, m => dup2 n (rec n (m + 1))
+decreasing_by
+  trace "Tactic is run (ideally only twice, in most general context)"
+  trace_state
+  decreasing_tactic
+
+end TestingGuessLex

tests/lean/issue2981.lean.expected.out

@@ -22,3 +22,24 @@ Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
+Tactic is run (ideally only once, in most general context)
+Tactic is run (ideally only once, in most general context)
+n : Nat
+⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
+n : Nat h : n ≠ n ⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
+Tactic is run (ideally only twice, in most general context)
+Tactic is run (ideally only twice, in most general context)
+Tactic is run (ideally only twice, in most general context)
+Tactic is run (ideally only twice, in most general context)
+n : Nat
+⊢ sizeOf n < sizeOf (Nat.succ n)
+n : Nat
+h : n ≠ n
+⊢ sizeOf n < sizeOf (Nat.succ n)
+n m : Nat
+⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
+    { fst := Nat.succ n, snd := m }
+n m : Nat
+h : n ≠ n
+⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
+    { fst := Nat.succ n, snd := m }