Lean4
/-- The goal of `field_simp` is to bring expressions in (semi-)fields over a common denominator, i.e. to
reduce them to expressions of the form `n / d` where neither `n` nor `d` contains any division
symbol. For example, `x / (1 - y) / (1 + y / (1 - y))` is reduced to `x / (1 - y + y)`:
```
example (x y z : ℚ) (hy : 1 - y ≠ 0) :
⌊x / (1 - y) / (1 + y / (1 - y))⌋ < 3 := by
field_simp
-- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
```
The `field_simp` tactic will also clear denominators in field *(in)equalities*, by
cross-multiplying. For example, `field_simp` will clear the `x` denominators in the following
equation:
```
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
(x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
field_simp
-- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
```
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,
`positivity` and `norm_num`, and will also use any nonzeroness/positivity proofs included explicitly
(e.g. `field_simp [hx]`). If your expression is not completely reduced by `field_simp`, check the
denominators of the resulting expression and provide proofs that they are nonzero/positive to enable
further progress.
-/
@[tactic_parser 1000]
public meta def fieldSimp : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.FieldSimp.fieldSimp 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "field_simp" false✝)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.discharger))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.simpArgs))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
