Commit 2025-12-17 02:05 e34e9538

feat(Linter/FlexibleLinter): generate Try this: simp only suggestions (#32425) When the flexible linter detects a simp or simp_all (without only) followed by a rigid tactic, it now:

• re-runs simp in the original context to capture the used theorems
• generates an actionable "Try this: simp only [...]" suggestion that users can click to apply This is a follow-up to #32421, which added the actionable warning message. This PR directly provides a fix. Example output:

warning: 'simp' is a flexible tactic modifying '⊢'. Try 'simp?' and use the suggested 'simp only [...]'.
Note: This linter can be disabled with `set_option linter.flexible false`