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:

```lean4
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
```

Co-authored-by: Edward van de Meent <edwardvdmeent@gmail.com>

Author: edegeltje

Mathlib/CategoryTheory/Idempotents/Basic.lean

@@ -60,8 +60,7 @@ the equalizer of the identity and this idempotent exists. -/
 theorem isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent :
     IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p := by
   constructor
-  · intro
-    intro X p hp
+  · intro _ X p hp
     rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
     exact
       ⟨Nonempty.intro

Mathlib/CategoryTheory/Limits/MonoCoprod.lean

@@ -76,8 +76,7 @@ theorem mono_inl_iff {A B : C} {c₁ c₂ : BinaryCofan A B} (hc₁ : IsColimit
     ∀ (c₁ c₂ : BinaryCofan A B) (_ : IsColimit c₁) (_ : IsColimit c₂) (_ : Mono c₁.inl),
       Mono c₂.inl
     by exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
-  intro c₁ c₂ hc₁ hc₂
-  intro
+  intro c₁ c₂ hc₁ hc₂ _
   simpa only [IsColimit.comp_coconePointUniqueUpToIso_hom] using
     mono_comp c₁.inl (hc₁.coconePointUniqueUpToIso hc₂).hom
 

Mathlib/CategoryTheory/Sites/Coverage.lean

@@ -288,8 +288,8 @@ it is the infimum of all Grothendieck topologies whose associated coverage conta
 theorem toGrothendieck_eq_sInf (K : Coverage C) : toGrothendieck _ K =
     sInf {J | K ≤ ofGrothendieck _ J } := by
   apply le_antisymm
-  · apply le_sInf; intro J hJ
-    intro X S hS
+  · apply le_sInf
+    intro J hJ X S hS
     induction hS with
     | of X S hS => apply hJ; assumption
     | top => apply J.top_mem

Mathlib/Data/PNat/Prime.lean

@@ -125,8 +125,7 @@ theorem dvd_prime {p m : ℕ+} (pp : p.Prime) : m ∣ p ↔ m = 1 ∨ m = p := b
   simp
 
 theorem Prime.ne_one {p : ℕ+} : p.Prime → p ≠ 1 := by
-  intro pp
-  intro contra
+  intro pp contra
   apply Nat.Prime.ne_one pp
   rw [PNat.coe_eq_one_iff]
   apply contra

Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean

@@ -84,8 +84,7 @@ theorem recF_eq_of_wEquiv (α : TypeVec n) {β : Type u} (u : F (α.append1 β)
   apply q.P.w_cases _ x
   intro a₀ f'₀ f₀
   apply q.P.w_cases _ y
-  intro a₁ f'₁ f₁
-  intro h
+  intro a₁ f'₁ f₁ h
   -- Porting note: induction on h doesn't work.
   refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_
   · intro a f' f₀ f₁ _h ih; simp only [recF_eq]

Mathlib/Order/Category/NonemptyFinLinOrd.lean

@@ -120,8 +120,7 @@ def dualEquiv : NonemptyFinLinOrd ≌ NonemptyFinLinOrd where
 theorem mono_iff_injective {A B : NonemptyFinLinOrd.{u}} (f : A ⟶ B) :
     Mono f ↔ Function.Injective f := by
   refine ⟨?_, ConcreteCategory.mono_of_injective f⟩
-  intro
-  intro a₁ a₂ h
+  intro _ a₁ a₂ h
   let X := of (ULift (Fin 1))
   let g₁ : X ⟶ A := ofHom ⟨fun _ => a₁, fun _ _ _ => by rfl⟩
   let g₂ : X ⟶ A := ofHom ⟨fun _ => a₂, fun _ _ _ => by rfl⟩

Mathlib/Order/OmegaCompletePartialOrder.lean

@@ -585,8 +585,7 @@ theorem ωSup_bind {β γ : Type v} (c : Chain α) (f : α →o Part β) (g : α
     simp only [Part.mem_bind_iff, Chain.map_coe,
       Function.comp_apply, OrderHom.partBind_coe]
     exact ⟨_, hb, hy⟩
-  · intro i
-    intro y hy
+  · intro i y hy
     simp only [Part.mem_bind_iff, Chain.map_coe,
       Function.comp_apply, OrderHom.partBind_coe] at hy
     rcases hy with ⟨b, hb₀, hb₁⟩

Mathlib/RingTheory/RootsOfUnity/Minpoly.lean

@@ -171,8 +171,7 @@ theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.Coprime m n) :
   · intro u hunit _ _
     congr
     simp [Nat.isUnit_iff.mp hunit]
-  · intro a p _ hprime
-    intro hind h hcop
+  · intro a p _ hprime hind h hcop
     rw [hind h (Nat.Coprime.coprime_mul_left hcop)]; clear hind
     replace hprime := hprime.nat_prime
     have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anne Baanen
+Authors: Anne Baanen, Edward van de Meent
 -/
 import Mathlib.Tactic.TacticAnalysis
 import Mathlib.Tactic.ExtractGoal
@@ -183,3 +183,30 @@ def terminalToGrind : TacticAnalysis.Config where
       logWarningAt stx m!"replace the proof with 'grind': {seq}"
       if oldHeartbeats * 2 < newHeartbeats then
         logWarningAt stx m!"'grind' is slower than the original: {oldHeartbeats} -> {newHeartbeats}"
+
+-- TODO: add compatibility with `rintro` and `intros`
+/-- Suggest merging two adjacent `intro` tactics which don't pattern match. -/
+register_option linter.tacticAnalysis.introMerge : Bool := {
+  defValue := true
+}
+
+@[tacticAnalysis linter.tacticAnalysis.introMerge, inherit_doc linter.tacticAnalysis.introMerge]
+def introMerge : TacticAnalysis.Config := .ofComplex {
+  out := Option (TSyntax `tactic)
+  ctx := Array (Array Term)
+  trigger ctx stx :=
+    match stx with
+    | `(tactic| intro%$x $args*) => .continue ((ctx.getD #[]).push
+      -- if `intro` is used without arguments, treat it as `intro _`
+      <| if args.size = 0 then #[⟨mkHole x⟩] else args)
+    | _ => if let some args := ctx then if args.size > 1 then .accept args else .skip else .skip
+  test ctx goal := do
+    let ctxT := ctx.flatten
+    let tac ← `(tactic| intro $ctxT*)
+    try
+      let _ ← Lean.Elab.runTactic goal tac
+      return some tac
+    catch _e => -- if for whatever reason we can't run `intro` here.
+      return none
+  tell _stx _old _oldHeartbeats new _newHeartbeats :=
+    if let some tac := new then m!"Try this: {tac}" else none}

MathlibTest/TacticAnalysis.lean

@@ -74,3 +74,36 @@ example {α : Type u} (f : α → Type max u v) : 1 = 1 := by
   rfl
 
 end replaceWithGrind
+
+section introMerge
+
+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
+
+/-- warning: Try this: intro _ b -/
+#guard_msgs in
+example : ∀ a b : Unit, a = b := by
+  intro
+  intro b
+  rfl
+
+/-- warning: Try this: intro a _ -/
+#guard_msgs in
+example : ∀ a b : Unit, a = b := by
+  intro a
+  intro _
+  rfl
+
+
+#guard_msgs in
+example : ∀ a b : Unit, a = b := by
+  intro a b
+  rfl
+
+end introMerge