feat: field tactic (leanprover-community#29089)

This PR creates a `field` tactic, i.e. an analogue of `ring` but for fields -- a finishing tactic for equality goals in fields.  It is basically `field_simp; ring1`, with a few tweaks for better error reporting!

We could have done this at any point in the last five years, but since `field_simp` is more performant as of leanprover-community#28658, now seems like a good time.

I propose that `field` be preferred to terminal `field_simp`/`field_simp; ring` from now on. I'll follow up with a PR ([preview](leanprover-community@44c0136)) making this change widely across the library. In the current PR I also rewrote the docstrings of `field_simp` and friends to nudge users in this direction.

Closes leanprover-community#4837

Author: hrmacbeth

Mathlib.lean

@@ -6168,6 +6168,7 @@ import Mathlib.Tactic.ExtractLets
 import Mathlib.Tactic.FBinop
 import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FastInstance
+import Mathlib.Tactic.Field
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.FieldSimp.Attr
 import Mathlib.Tactic.FieldSimp.Discharger

Mathlib/Tactic.lean

@@ -87,6 +87,7 @@ import Mathlib.Tactic.ExtractLets
 import Mathlib.Tactic.FBinop
 import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FastInstance
+import Mathlib.Tactic.Field
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.FieldSimp.Attr
 import Mathlib.Tactic.FieldSimp.Discharger

Mathlib/Tactic/Field.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2025 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth
+-/
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Ring.Basic
+
+
+/-! # A tactic for proving algebraic goals in a field
+
+This file contains the `field` tactic, a finishing tactic which roughly consists of running
+`field_simp; ring1`.
+
+-/
+
+open Lean Meta Qq
+
+namespace Mathlib.Tactic.FieldSimp
+
+open Lean Elab Tactic Lean.Parser.Tactic
+
+/--
+The `field` tactic proves equality goals in (semi-)fields. For example:
+```
+example {x y : ℚ} (hx : x + y ≠ 0) : x / (x + y) + y / (x + y) = 1 := by
+  field
+example {a b : ℝ} (ha : a ≠ 0) : a / (a * b) - 1 / b = 0 := by field
+```
+The scope of the tactic is equality goals which are *universal*, in the sense that they are true in
+any field in which the appropriate denominators don't vanish. (That is, they are consequences purely
+of the field axioms.)
+
+Checking the nonvanishing of the necessary denominators is done using a variety of tricks -- in
+particular this part of the reasoning is non-universal, i.e. can be specific to the field at hand
+(order properties, explicit `≠ 0` hypotheses, `CharZero` if that is known, etc).  The user can also
+provide additional terms to help with the nonzeroness proofs. For example:
+```
+example {K : Type*} [Field K] (hK : ∀ x : K, x ^ 2 + 1 ≠ 0) (x : K) :
+    1 / (x ^ 2 + 1) + x ^ 2 / (x ^ 2 + 1) = 1 := by
+  field [hK]
+```
+
+The `field` tactic is built from the tactics `field_simp` (which clears the denominators) and `ring`
+(which proves equality goals universally true in commutative (semi-)rings). If `field` fails to
+prove your goal, you may still be able to prove your goal by running the `field_simp` and `ring_nf`
+normalizations in some order.  For example, this statement:
+```
+example {a b : ℚ} (H : b + a ≠ 0) : a / (a + b) + b / (b + a) = 1
+```
+is not proved by `field` but is proved by `ring_nf at *; field`. -/
+elab (name := field) "field" d:(ppSpace discharger)? args:(ppSpace simpArgs)? : tactic =>
+    withMainContext do
+  let disch ← parseDischarger d args
+  let s0 ← saveState
+  -- run `field_simp` (only at the top level, not recursively)
+  liftMetaTactic1 (transformAtTarget ((AtomM.run .reducible ∘ reduceProp disch) ·) "field"
+    (failIfUnchanged := False) · default)
+  let s1 ← saveState
+  try
+    -- run `ring1`
+    liftMetaFinishingTactic fun g ↦ AtomM.run .reducible <| Ring.proveEq g
+  catch e =>
+    try
+      -- If `field` doesn't solve the goal, we first backtrack to the situation at the time of the
+      -- `field_simp` call, and suggest `field_simp` if `field_simp` does anything useful.
+      s0.restore
+      let tacticStx ← `(tactic| field_simp $(d)? $(args)?)
+      evalTactic tacticStx
+      Meta.Tactic.TryThis.addSuggestion (← getRef) tacticStx
+    catch _ =>
+      -- If `field_simp` also doesn't do anything useful (maybe there are no denominators in the
+      -- goal), then we backtrack to where the `ring1` call failed, and report that error message.
+      s1.restore
+      throw e
+
+end Mathlib.Tactic.FieldSimp
+
+/-! We register `field` with the `hint` tactic. -/
+register_hint field

Mathlib/Tactic/FieldSimp.lean

@@ -684,6 +684,10 @@ example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
   -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
 ```
 
+A very common pattern is `field_simp; ring` (clear denominators, then the resulting goal is
+solvable by the axioms of a commutative ring). The finishing tactic `field` is a shorthand for this
+pattern.
+
 Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
 side conditions. The `field_simp` tactic attempts to discharge these, and will omit such steps if it
 cannot discharge the corresponding side conditions. The discharger will try, among other things,

MathlibTest/FieldSimp.lean

@@ -3,13 +3,13 @@ Copyright (c) 2022 Jon Eugster. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster, David Renshaw, Heather Macbeth, Michael Rothgang
 -/
-import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Field
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Ring
 import Mathlib.Data.Real.Basic
 
 /-!
-# Tests for the `field_simp` tactic
+# Tests for the `field_simp` and `field` tactics
 -/
 
 private axiom test_sorry : ∀ {α}, α
@@ -370,16 +370,17 @@ end
 
 /-! ## Cancel denominators from equalities -/
 
-/-! ### Most common use case: Cancel denominators to something solvable by `ring`
+/-! ### Finishing tactic
 
-When (eventually) this is robust enough, there should be a `field` tactic
+The `field` tactic is a finishing tactic for equalities in fields.
+Effectively it runs `field_simp` to clear denominators, then hands the result to `ring1`.
 -/
 
-macro "field" : tactic => `(tactic | (try field_simp) <;> ring1)
-
 example : (1:ℚ) / 3 + 1 / 6 = 1 / 2 := by field
 example {x : ℚ} (hx : x ≠ 0) : x * x⁻¹ = 1 := by field
 example {a b : ℚ} (h : b ≠ 0) : a / b + 2 * a / b + (-a) / b + (- (2 * a)) / b = 0 := by field
+
+-- example from the `field` docstring
 example {x y : ℚ} (hx : x + y ≠ 0) : x / (x + y) + y / (x + y) = 1 := by field
 
 example {x : ℚ} : x ^ 2 / (x ^ 2 + 1) + 1 / (x ^ 2 + 1) = 1 := by field
@@ -392,14 +393,67 @@ example {K : Type*} [Field K] (a b c d x y : K) (hx : x ≠ 0) (hy : y ≠ 0) :
     a + b / x + c / x ^ 2 + d / x ^ 3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) := by
   field
 
+-- example from the `field` docstring
 example {a b : ℚ} (ha : a ≠ 0) : a / (a * b) - 1 / b = 0 := by field
+
 example {x : ℚ} : x ^ 2 * x⁻¹ = x := by field
 
+-- example from `field` docstring
+example {K : Type*} [Field K] (hK : ∀ x : K, x ^ 2 + 1 ≠ 0) (x : K) :
+    1 / (x ^ 2 + 1) + x ^ 2 / (x ^ 2 + 1) = 1 := by
+  field [hK]
+
 -- testing that mdata is cleared before parsing goal
 example {x : ℚ} (hx : x ≠ 0) : x * x⁻¹ = 1 := by
   have : 1 = 1 := rfl
   field
 
+-- `field` will suggest `field_simp` on failure, if `field_simp` does anything.
+
+/--
+info: Try this:
+  field_simp
+---
+error: unsolved goals
+x y z : ℚ
+hx : x + y ≠ 0
+⊢ 1 = z
+-/
+#guard_msgs in
+example {x y z : ℚ} (hx : x + y ≠ 0) : x / (x + y) + y / (x + y) = z := by field
+
+-- If `field` fails but `field_simp` also fails, we just throw an error.
+/--
+error: ring failed, ring expressions not equal
+x y z : ℚ
+⊢ x + y = z
+-/
+#guard_msgs in
+example {x y z : ℚ} : x + y = z := by field
+
+/-
+The `field` tactic differs slightly from `field_simp; ring1` in that it clears denominators only at
+the top level, not recursively in subexpressions.
+
+(`ring1` acts only at the top level, so for consistency we also clear denominators only at the top
+level.) -/
+/--
+info: Try this:
+  field_simp
+---
+error: unsolved goals
+a b : ℚ
+f : ℚ → ℚ
+⊢ f (a * b) * (1 - 1) = 0
+-/
+#guard_msgs in
+example (a b : ℚ) (f : ℚ → ℚ) : f (a ^ 2 * b / a) - f (b ^ 2 * a / b) = 0 := by field
+
+-- (Compare with the example above: this is out of scope for `field`.)
+example (a b : ℚ) (f : ℚ → ℚ) : f (a ^ 2 * b / a) - f (b ^ 2 * a / b) = 0 := by
+  field_simp
+  ring1
+
 /-! ### Mid-proof use -/
 
 example {K : Type*} [Semifield K] (x y : K) (hy : y + 1 ≠ 0) : 2 * x / (y + 1) = x := by
@@ -535,9 +589,10 @@ normalize properly.
 It is not clear whether or not this iterated alternation always achieves the "obvious" normalization
 eventually. Nor is it clear whether, if so, there are any bounds on how many iterations are needed.
 -/
-section
 
 -- modified from 2021 American Mathematics Competition 12B, problem 9
+section
+
 example (P : ℝ → Prop) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
     P ((4 * x + y) / x / (x / (3 * x + y)) - (5 * x + y) / x / (x / (2 * x + y))) := by
   ring_nf
@@ -562,6 +617,77 @@ example (P : ℝ → Prop) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 
 end
 
+section
+
+-- This example is used in the `field` docstring.
+example {a b : ℚ} (H : b + a ≠ 0) : a / (a + b) + b / (b + a) = 1 := by
+  ring_nf at *
+  field
+
+/--
+info: Try this:
+  field_simp
+---
+error: unsolved goals
+a b : ℚ
+H : b + a ≠ 0
+⊢ (a + b) / (a + b) = 1
+-/
+#guard_msgs in
+example {a b : ℚ} (H : b + a ≠ 0) : a / (a + b) + b / (b + a) = 1 := by
+  ring_nf
+  field
+
+/--
+info: Try this:
+  field_simp
+---
+error: unsolved goals
+a b : ℚ
+H : b + a ≠ 0
+⊢ a * (b + a) / (a + b) + b = b + a
+-/
+#guard_msgs in
+example {a b : ℚ} (H : b + a ≠ 0) : a / (a + b) + b / (b + a) = 1 := by
+  field
+
+example {a b : ℚ} (H : a + b + 1 ≠ 0) :
+    a / (a + (b + 1) ^ 2 / (b + 1)) + (b + 1) / (b + a + 1) = 1 := by
+  field_simp
+  ring_nf at *
+  field
+
+/--
+info: Try this:
+  field_simp
+---
+error: unsolved goals
+a b : ℚ
+H : 1 + a + b ≠ 0
+⊢ a * (1 + a + b) / (a + b * 2 / (1 + b) + b ^ 2 / (1 + b) + 1 / (1 + b)) + b + 1 = 1 + a + b
+-/
+#guard_msgs in
+example {a b : ℚ} (H : a + b + 1 ≠ 0) :
+    a / (a + (b + 1) ^ 2 / (b + 1)) + (b + 1) / (b + a + 1) = 1 := by
+  ring_nf at *
+  field
+
+/--
+info: Try this:
+  field_simp
+---
+error: unsolved goals
+a b : ℚ
+H : a + b + 1 ≠ 0
+⊢ a / (a + (b + 1)) + (b + 1) / (b + a + 1) = 1
+-/
+#guard_msgs in
+example {a b : ℚ} (H : a + b + 1 ≠ 0) :
+    a / (a + (b + 1) ^ 2 / (b + 1)) + (b + 1) / (b + a + 1) = 1 := by
+  field
+
+end
+
 /-! From PluenneckeRuzsa: new `field_simp` doesn't handle variable exponents -/
 
 example (x y : ℚ≥0) (n : ℕ) (hx : x ≠ 0) : y * ((y / x) ^ n * x) = (y / x) ^ (n + 1) * x * x := by