Lean4
/-- The goal of the `field_simp` conv tactic is to bring an expression in a (semi-)field over a common
denominator, i.e. to reduce it to an expression 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
conv => enter [1, 1]; field_simp
-- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
```
As in this example, cancelling and combining denominators will generally require checking
"nonzeroness" 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 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 to
enable further progress.
The `field_simp` conv tactic is a variant of the main (i.e., not conv) `field_simp` tactic. The
latter operates recursively on subexpressions, bringing *every* field-expression encountered to the
form `n / d`.
-/
@[conv_parser 1000]
public meta def convField_simp__ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.FieldSimp.convField_simp__ 1022
(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))
