Commit 2025-09-13 11:53 f7753964

feat(TacticAnalysis): add a linter for merging consequent intro tactics (#28862) The linter is triggered by setting the option linter.tacticAnalysis.introMerge (which is on by default). When it finds consequent intro tactics, it will give a warning suggesting a single use of intro. For example:

set_option linter.tacticAnalysis.introMerge true
/-- warning: Try this: intro a b -/
#guard_msgs in
example : ∀ a b : Unit, a = b := by
  intro a
  intro b
  rfl