# Discharger for `field_simp` tactic #

The `field_simp` tactic (implemented downstream from this file) clears denominators in algebraic expressions. In order to do this, the denominators need to be certified as nonzero. This file contains the discharger which carries out these checks.

Currently the discharger tries four strategies:

1. `assumption`
2. `positivity`
3. `norm_num`
4. `simp` with the same simp-context as the `field_simp` call which invoked it

TODO: Ideally the discharger would be just `positivity` (which, despite the name, has robust handling of general `≠ 0` goals, not just `> 0` goals). We need the other strategies currently to get (a cheap approximation of) `positivity` on fields without a partial order.

The refactor of `positivity` to avoid a partial order assumption would be large but not fundamentally difficult.

### Main declarations #

- `Mathlib.Tactic.FieldSimp.discharge`: the discharger, of type `Expr → SimpM (Option Expr)`

- `field_simp_discharge`: tactic syntax for the discharger (most useful for testing/debugging)

source
partial def Mathlib.Tactic.FieldSimp.discharge (prop : Lean.Expr) :
Lean.Meta.SimpM (Option Lean.Expr)

Discharge strategy for the `field_simp` tactic.

source
def Mathlib.Tactic.FieldSimp.tacticField_simp_discharge :
Lean.ParserDescr

Discharge strategy for the `field_simp` tactic.

Equations

- One or more equations did not get rendered due to their size.

Instances For