field_simp tactic

Tactic to clear denominators in algebraic expressions.

Lists of expressions representing exponents and atoms, and operations on such lists

@[reducible, inline]

abbrev Mathlib.Tactic.FieldSimp.qNF {v : Lean.Level} (M : Q(Type v)) : Type

Basic meta-code "normal form" object of the field_simp tactic: a type synonym for a list of ordered triples comprising an expression representing a term of a type M (where typically M is a field), together with an integer "power" and a natural number "index".

The natural number represents the index of the M term in the AtomM monad: this is not enforced, but is sometimes assumed in operations. Thus when items ((a₁, x₁), k) and ((a₂, x₂), k) appear in two different FieldSimp.qNF objects (i.e. with the same ℕ-index k), it is expected that the expressions x₁ and x₂ are the same. It is also expected that the items in a FieldSimp.qNF list are in strictly decreasing order by natural-number index.

By forgetting the natural number indices, an expression representing a Mathlib.Tactic.FieldSimp.NF object can be built from a FieldSimp.qNF object; this construction is provided as Mathlib.Tactic.FieldSimp.qNF.toNF.

Equations

• Mathlib.Tactic.FieldSimp.qNF M = List ((ℤ × Q(«$M»)) × ℕ)

def Mathlib.Tactic.FieldSimp.qNF.toNF {v : Lean.Level} {M : Q(Type v)} (l : qNF q(«$M»)) : Q(NF «$M»)

Given l of type qNF M, i.e. a list of (ℤ × Q($M)) × ℕs (two Exprs and a natural number), build an Expr representing an object of type NF M (i.e. List (ℤ × M)) in the in the obvious way: by forgetting the natural numbers and gluing together the integers and Exprs.

Equations

• l.toNF = List.foldr (fun (x : (ℤ × Q(«$M»)) × ℕ) (l : Q(Mathlib.Tactic.FieldSimp.NF «$M»)) => match x with | ((a, x), snd) => q((«$a», «$x») ::ᵣ «$l»)) q([]) l

def Mathlib.Tactic.FieldSimp.qNF.onExponent {v : Lean.Level} {M : Q(Type v)} (l : qNF M) (f : ℤ → ℤ) : qNF M

Given l of type qNF M, i.e. a list of (ℤ × Q($M)) × ℕs (two Exprs and a natural number), apply an expression representing a function with domain ℤ to each of the ℤ components.

Equations

• l.onExponent f = List.map (fun (x : (ℤ × Q(«$M»)) × ℕ) => match x with | ((a, x), k) => ((f a, x), k)) l

def Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial {v : Lean.Level} {M : Q(Type v)} (iM : Q(GroupWithZero «$M»)) (r : ℤ) (x : Q(«$M»)) : Lean.MetaM ((e : Q(«$M»)) × Q(zpow' «$x» «$r» = «$e»))

Build a transparent expression for the product of powers represented by l : qNF M.

Equations

• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM 0 x = pure ⟨q(«$x» / «$x»), q(⋯)⟩
• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM 1 x = pure ⟨x, q(⋯)⟩
• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM (Int.ofNat r_2) x = do let pf ← Qq.mkDecideProofQ q(«$r_2» ≠ 0) pure ⟨q(«$x» ^ «$r_2»), q(⋯)⟩
• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM r x = do let pf ← Qq.mkDecideProofQ q(«$r» ≠ 0) pure ⟨q(«$x» ^ «$r»), q(⋯)⟩

def Mathlib.Tactic.FieldSimp.qNF.tryClearZero {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (r : ℤ) (x : Q(«$M»)) (i : ℕ) (l : qNF M) : Lean.MetaM ((l' : qNF M) × have a := l'.toNF; have a_1 := toNF (((r, x), i) :: l); Q(«$a_1».eval = «$a».eval))

Try to drop an expression zpow' x r from the beginning of a product. If r ≠ 0 this of course can't be done. If r = 0, then zpow' x r is equal to x / x, so it can be simplified to 1 (hence dropped from the beginning of the product) if we can find a proof that x ≠ 0.

Equations

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

def Mathlib.Tactic.FieldSimp.qNF.removeZeros {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (l : qNF M) : Lean.MetaM ((l' : qNF M) × have a := l'.toNF; have a_1 := l.toNF; Q(«$a_1».eval = «$a».eval))

Given l : qNF M, obtain l' : qNF M by removing all l's exponent-zero entries where the corresponding atom can be proved nonzero, and construct a proof that their associated expressions are equal.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.removeZeros disch iM [] = pure ⟨[], q(⋯)⟩

def Mathlib.Tactic.FieldSimp.qNF.split {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l : qNF M) : Lean.MetaM ((l_n : qNF M) × (l_d : qNF M) × have a := l_d.toNF; have a_1 := l_n.toNF; have a_2 := l.toNF; Q(«$a_2».eval = «$a_1».eval / «$a».eval))

Given a product of powers, split as a quotient: the positive powers divided by (the negations of) the negative powers.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.split iM [] = pure ⟨[], ⟨[], q(⋯)⟩⟩

def Mathlib.Tactic.FieldSimp.qNF.evalPretty {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l : qNF M) : Lean.MetaM ((e : Q(«$M»)) × have a := l.toNF; Q(«$a».eval = «$e»))

Build a transparent expression for the product of powers represented by l : qNF M.

Equations

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

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.mul {v : Lean.Level} {M : Q(Type v)} : qNF q(«$M») → qNF q(«$M») → qNF q(«$M»)

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), construct another such term l, which will have the property that in the field $M, the product of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by l.

The construction assumes, to be valid, that the lists l₁ and l₂ are in strictly decreasing order by ℕ-component, and that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then the expressions x₁ and x₂ are equal.

The construction is as follows: merge the two lists, except that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then contribute a term (a₁ + a₂, x₁) to the output list with ℕ-component k.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.mul [] x✝ = x✝
• x✝.mul [] = x✝

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.mkMulProof {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : qNF M) : have a := (l₁.mul l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval * «$a_1».eval = «$a».eval)

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), recursively construct a proof that in the field $M, the product of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by FieldSimp.qNF.mul l₁ l₁.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM [] l₂ = q(⋯)
• Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM l₁ [] = q(⋯)

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.div {v : Lean.Level} {M : Q(Type v)} : qNF M → qNF M → qNF M

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), construct another such term l, which will have the property that in the field $M, the quotient of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by l.

The construction assumes, to be valid, that the lists l₁ and l₂ are in strictly decreasing order by ℕ-component, and that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then the expressions x₁ and x₂ are equal.

The construction is as follows: merge the first list and the negation of the second list, except that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then contribute a term (a₁ - a₂, x₁) to the output list with ℕ-component k.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.div [] x✝ = x✝.onExponent Neg.neg
• x✝.div [] = x✝

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.mkDivProof {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : qNF M) : have a := (l₁.div l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval / «$a_1».eval = «$a».eval)

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), recursively construct a proof that in the field $M, the quotient of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by FieldSimp.qNF.div l₁ l₁.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM [] l₂ = q(⋯)
• Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM l₁ [] = q(⋯)

inductive Mathlib.Tactic.FieldSimp.DenomCondition {v : Lean.Level} {M : Q(Type v)} (iM : Q(GroupWithZero «$M»)) : Type

Constraints on denominators which may need to be considered in field_simp: no condition, nonzeroness, or strict positivity.

• none {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} : DenomCondition iM
• nonzero {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} : DenomCondition iM
• positive {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} (iM' : Q(PartialOrder «$M»)) (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLT «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»)) : DenomCondition iM

def Mathlib.Tactic.FieldSimp.DenomCondition.proof {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} (L : qNF M) : DenomCondition iM → Type

Given a field-simp-normal-form expression L (a product of powers of atoms), a proof (according to the value of DenomCondition) of that expression's nonzeroness, strict positivity, etc.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.DenomCondition.proof L Mathlib.Tactic.FieldSimp.DenomCondition.none = Unit

def Mathlib.Tactic.FieldSimp.DenomCondition.proofZero {v : Lean.Level} {M : Q(Type v)} {iM : Q(CommGroupWithZero «$M»)} (cond : DenomCondition q(inferInstance)) : proof [] cond

The empty field-simp-normal-form expression [] (representing 1 as an empty product of powers of atoms) can be proved to be nonzero, strict positivity, etc., as needed, as specified by the value of DenomCondition.

Equations

• Mathlib.Tactic.FieldSimp.DenomCondition.none.proofZero = ()
• Mathlib.Tactic.FieldSimp.DenomCondition.nonzero.proofZero = q(⋯)
• (Mathlib.Tactic.FieldSimp.DenomCondition.positive iM' iM'' iM''' iM'''').proofZero = q(⋯)

def Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc {v : Lean.Level} {M : Q(Type v)} {iM : Q(CommGroupWithZero «$M»)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) {cond : DenomCondition q(inferInstance)} {L : qNF M} (hL : DenomCondition.proof L cond) (e : Q(«$M»)) (r : ℤ) (i : ℕ) : Lean.MetaM (Q(«$e» ≠ 0) × DenomCondition.proof (((r, e), i) :: L) cond)

Given a proof of the nonzeroness, strict positivity, etc. (as specified by the value of DenomCondition) of a field-simp-normal-form expression L (a product of powers of atoms), construct a corresponding proof for ((r, e), i) :: L.

In this version we also expose the proof of nonzeroness of e.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc disch hL_2 e r i = do let __do_lift ← disch q(«$e» ≠ 0) pure (__do_lift, ())
• Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc disch hL_2 e r i = do let pf ← disch q(«$e» ≠ 0) have pf₀ : have a := L.toNF; Q(«$a».eval ≠ 0) := hL_2 pure (pf, q(⋯))

def Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' {v : Lean.Level} {M : Q(Type v)} {iM : Q(CommGroupWithZero «$M»)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) {cond : DenomCondition q(inferInstance)} {L : qNF M} (hL : DenomCondition.proof L cond) (e : Q(«$M»)) (r : ℤ) (i : ℕ) : Lean.MetaM (DenomCondition.proof (((r, e), i) :: L) cond)

Given a proof of the nonzeroness, strict positivity, etc. (as specified by the value of DenomCondition) of a field-simp-normal-form expression L (a product of powers of atoms), construct a corresponding proof for ((r, e), i) :: L.

Equations

• Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' disch hL_2 e r i = pure ()
• Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' disch hL_2 e r i = do let pf ← disch q(«$e» ≠ 0) have pf₀ : have a := L.toNF; Q(«$a».eval ≠ 0) := hL_2 pure q(⋯)
• Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' disch hL_2 e r i = do let pf ← disch q(0 < «$e») have pf₀ : have a := L.toNF; Q(0 < «$a».eval) := hL_2 pure q(⋯)

partial def Mathlib.Tactic.FieldSimp.qNF.gcd {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : qNF M) (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (cond : DenomCondition q(inferInstance)) : Lean.MetaM ((L : qNF M) × (l₁' : qNF M) × (l₂' : qNF M) × (have a := l₁.toNF; have a_1 := l₁'.toNF; have a_2 := L.toNF; Q(«$a_2».eval * «$a_1».eval = «$a».eval)) × (have a := l₂.toNF; have a_1 := l₂'.toNF; have a_2 := L.toNF; Q(«$a_2».eval * «$a_1».eval = «$a».eval)) × DenomCondition.proof L cond)

Extract a common factor L of two products-of-powers l₁ and l₂ in M, in the sense that both l₁ and l₂ are quotients by L of products of positive powers.

The variable cond specifies whether we extract a certified nonzero[/positive] (and therefore potentially smaller) common factor. If so, the metaprogram returns a "proof" that this common factor is nonzero/positive, i.e. an expression Q(NF.eval $(L.toNF) ≠ 0) / Q(0 < NF.eval $(L.toNF)).

Core of the field_simp tactic

partial def Mathlib.Tactic.FieldSimp.normalize {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (x : Q(«$M»)) : AtomM ((y : Q(«$M»)) × ((g : Sign M) × have a := g.expr y; Q(«$x» = «$a»)) × (l : qNF M) × have a := l.toNF; Q(«$y» = «$a».eval))

The main algorithm behind the field_simp tactic: partially-normalizing an expression in a field M into the form x1 ^ c1 * x2 ^ c2 * ... x_k ^ c_k, where x1, x2, ... are distinct atoms in M, and c1, c2, ... are integers.

def Mathlib.Tactic.FieldSimp.reduceExprQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (x : Q(«$M»)) : AtomM ((x' : Q(«$M»)) × Q(«$x» = «$x'»))

Given x in a commutative group-with-zero, construct a new expression in the standard form *** / *** (all denominators at the end) which is equal to x.

Equations

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

def Mathlib.Tactic.FieldSimp.reduceEqQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (e₁ e₂ : Q(«$M»)) : AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» = «$e₂») = («$f₁» = «$f₂»)))

Given e₁ and e₂, cancel nonzero factors to construct a new equality which is logically equivalent to e₁ = e₂.

Equations

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

def Mathlib.Tactic.FieldSimp.reduceLeQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (iM' : Q(PartialOrder «$M»)) (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLE «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»)) (e₁ e₂ : Q(«$M»)) : AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» ≤ «$e₂») = («$f₁» ≤ «$f₂»)))

Given e₁ and e₂, cancel positive factors to construct a new inequality which is logically equivalent to e₁ ≤ e₂.

Equations

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

def Mathlib.Tactic.FieldSimp.reduceLtQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (iM' : Q(PartialOrder «$M»)) (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLT «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»)) (e₁ e₂ : Q(«$M»)) : AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» < «$e₂») = («$f₁» < «$f₂»)))

Given e₁ and e₂, cancel positive factors to construct a new inequality which is logically equivalent to e₁ < e₂.

Equations

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

def Mathlib.Tactic.FieldSimp.reduceExpr (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (x : Lean.Expr) : AtomM Lean.Meta.Simp.Result

Given x in a commutative group-with-zero, construct a new expression in the standard form *** / *** (all denominators at the end) which is equal to x.

def Mathlib.Tactic.FieldSimp.reduceProp (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (t : Lean.Expr) : AtomM Lean.Meta.Simp.Result

Given an (in)equality a = b (respectively, a ≤ b, a < b), cancel nonzero (resp. positive) factors to construct a new (in)equality which is logically equivalent to a = b (respectively, a ≤ b, a < b).

Frontend

def Mathlib.Tactic.FieldSimp.parseDischarger (d : Option (Lean.TSyntax `Lean.Parser.Tactic.discharger)) (args : Option (Lean.TSyntax `Lean.Parser.Tactic.simpArgs)) : Lean.Elab.Tactic.TacticM ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»))

If the user provided a discharger, elaborate it. If not, we will use the field_simp_discharge default discharger, which (among other things) includes a simp-run for the specified argument list, so we elaborate those arguments.

Equations

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

def Mathlib.Tactic.FieldSimp.fieldSimp : Lean.ParserDescr

field_simp normalizes expressions in (semi-)fields by rewriting them to a common denominator, i.e. to reduce them to expressions of the form n / d where neither n nor d contains any division symbol. The field_simp tactic will also clear denominators in field (in)equalities, by cross-multiplying.

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.

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The default discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See field_simp_discharge for full details of the default discharger algorithm.

• field_simp at l1 l2 ... can be used to normalize at the given locations.
• field_simp (disch := tac) uses the tactic sequence tac to discharge nonzeroness/positivity proofs.
• field_simp [t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness/positivity proofs.

Examples:

-- `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`
  sorry

-- `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`
  sorry

Equations

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

def Mathlib.Tactic.FieldSimp.convField_simp__ : Lean.ParserDescr

field_simp normalizes an expression in a (semi-)field by rewriting it to 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.

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.

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The default discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See field_simp_discharge for full details of the default discharger algorithm.

• field_simp (disch := tac) uses the tactic sequence tac to discharge nonzeroness/positivity proofs.
• field_simp [t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness/positivity proofs.

Examples:

-- `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`

Equations

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

def Mathlib.Tactic.FieldSimp.proc : Lean.Meta.Simp.Simproc

field is a simp set that clears denominators in (semi-)field (in)equalities.

The field simp set is a variant of the field_simp tactic. The latter operates recursively on subexpressions, bringing every field-expression encountered to the form n / d, and then attempts to clear the denominator. (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See field_simp_discharge for full details of the discharger algorithm.

• simp [field, t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness/positivity proofs.

Examples:

example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

Equations

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

def fieldEq : Lean.Meta.Simp.Simproc

field is a simp set that clears denominators in (semi-)field (in)equalities.

The field simp set is a variant of the field_simp tactic. The latter operates recursively on subexpressions, bringing every field-expression encountered to the form n / d, and then attempts to clear the denominator. (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See field_simp_discharge for full details of the discharger algorithm.

• simp [field, t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness/positivity proofs.

Examples:

example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

Equations

• fieldEq = Mathlib.Tactic.FieldSimp.proc

def fieldLe : Lean.Meta.Simp.Simproc

field is a simp set that clears denominators in (semi-)field (in)equalities.

The field simp set is a variant of the field_simp tactic. The latter operates recursively on subexpressions, bringing every field-expression encountered to the form n / d, and then attempts to clear the denominator. (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See field_simp_discharge for full details of the discharger algorithm.

• simp [field, t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness/positivity proofs.

Examples:

example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

Equations

• fieldLe = Mathlib.Tactic.FieldSimp.proc

def fieldLt : Lean.Meta.Simp.Simproc

field is a simp set that clears denominators in (semi-)field (in)equalities.

The field simp set is a variant of the field_simp tactic. The latter operates recursively on subexpressions, bringing every field-expression encountered to the form n / d, and then attempts to clear the denominator. (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See field_simp_discharge for full details of the discharger algorithm.

• simp [field, t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness/positivity proofs.

Examples:

example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

Equations

• fieldLt = Mathlib.Tactic.FieldSimp.proc

We register field_simp with the hint tactic.