feat: register mathlib finishing tactics with try?

kim-em · kim-em · commit 3d04a0d8aac6 · 2025-12-08T11:34:54.000+11:00
Register a selection of mathlib finishing tactics with the `try?` tactic:
- Common finishing tactics: tauto, aesop, fun_prop
- Domain-specific finishing tactics: norm_num, noncomm_ring, field,
  bound, finiteness, compute_degree, positivity, field_simp

These tactics are registered alongside the existing `hint` registrations
to make them available to the built-in `try?` tactic in Lean 4.27.0+.

🤖 Prepared with Claude Code
diff --git a/Mathlib/Tactic/Bound.lean b/Mathlib/Tactic/Bound.lean
@@ -258,3 +258,4 @@ We register `bound` with the `hint` tactic.
 -/
 
 register_hint 70 bound
+register_try?_tactic (priority := 70) bound
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
@@ -151,3 +151,15 @@ register_hint 200 omega
 register_hint 200 fun_prop
 
 end Hint
+
+/-!
+# Register tactics with `try?`. Tactics with larger priority run first.
+-/
+
+section Try
+
+register_try?_tactic (priority := 500) tauto
+register_try?_tactic (priority := 80) aesop
+register_try?_tactic (priority := 200) fun_prop
+
+end Try
diff --git a/Mathlib/Tactic/ComputeDegree.lean b/Mathlib/Tactic/ComputeDegree.lean
@@ -529,3 +529,4 @@ end Mathlib.Tactic.ComputeDegree
  We register `compute_degree` with the `hint` tactic.
  -/
 register_hint 1000 compute_degree
+register_try?_tactic (priority := 1000) compute_degree
diff --git a/Mathlib/Tactic/Field.lean b/Mathlib/Tactic/Field.lean
@@ -82,3 +82,4 @@ end Mathlib.Tactic.FieldSimp
 
 /-! We register `field` with the `hint` tactic. -/
 register_hint 850 field
+register_try?_tactic (priority := 850) field
diff --git a/Mathlib/Tactic/FieldSimp.lean b/Mathlib/Tactic/FieldSimp.lean
@@ -792,3 +792,4 @@ attribute [field, inherit_doc FieldSimp.proc] fieldEq fieldLe fieldLt
  We register `field_simp` with the `hint` tactic.
  -/
 register_hint 1000 field_simp
+register_try?_tactic (priority := 1000) field_simp
diff --git a/Mathlib/Tactic/Finiteness.lean b/Mathlib/Tactic/Finiteness.lean
@@ -76,3 +76,4 @@ macro (name := finiteness_nonterminal) "finiteness_nonterminal" c:Aesop.tactic_c
  We register `finiteness` with the `hint` tactic.
  -/
 register_hint 1000 finiteness
+register_try?_tactic (priority := 1000) finiteness
diff --git a/Mathlib/Tactic/NoncommRing.lean b/Mathlib/Tactic/NoncommRing.lean
@@ -81,3 +81,4 @@ We register `noncomm_ring` with the `hint` tactic.
 -/
 
 register_hint 1000 noncomm_ring
+register_try?_tactic (priority := 1000) noncomm_ring
diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean
@@ -313,3 +313,4 @@ We register `norm_num` with the `hint` tactic.
 -/
 
 register_hint 1000 norm_num
+register_try?_tactic (priority := 1000) norm_num
diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean
@@ -536,3 +536,4 @@ We register `positivity` with the `hint` tactic.
 -/
 
 register_hint 1000 positivity
+register_try?_tactic (priority := 1000) positivity

Original file line number	Diff line number	Diff line change
@@ -258,3 +258,4 @@ We register `bound` with the `hint` tactic.
`258`	`258`	`-/`
`259`	`259`
`260`	`260`	`register_hint 70 bound`
	`261`	`+register_try?_tactic (priority := 70) bound`
Original file line number	Diff line number	Diff line change
`@@ -82,3 +82,4 @@ end Mathlib.Tactic.FieldSimp`
`82`	`82`
`83`	`83`	/-! We register `field` with the `hint` tactic. -/
`84`	`84`	`register_hint 850 field`
	`85`	`+register_try?_tactic (priority := 850) field`
Original file line number	Diff line number	Diff line change
@@ -81,3 +81,4 @@ We register `noncomm_ring` with the `hint` tactic.
`81`	`81`	`-/`
`82`	`82`
`83`	`83`	`register_hint 1000 noncomm_ring`
	`84`	`+register_try?_tactic (priority := 1000) noncomm_ring`
Original file line number	Diff line number	Diff line change
@@ -313,3 +313,4 @@ We register `norm_num` with the `hint` tactic.
`313`	`313`	`-/`
`314`	`314`
`315`	`315`	`register_hint 1000 norm_num`
	`316`	`+register_try?_tactic (priority := 1000) norm_num`
Original file line number	Diff line number	Diff line change
@@ -536,3 +536,4 @@ We register `positivity` with the `hint` tactic.
`536`	`536`	`-/`
`537`	`537`
`538`	`538`	`register_hint 1000 positivity`
	`539`	`+register_try?_tactic (priority := 1000) positivity`