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

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

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

• Mathlib.Tactic.FieldSimp.DenomCondition.proof L Mathlib.Tactic.FieldSimp.DenomCondition.none = Unit
• Mathlib.Tactic.FieldSimp.DenomCondition.proof L Mathlib.Tactic.FieldSimp.DenomCondition.nonzero = Q(Mathlib.Tactic.FieldSimp.NF.eval unknown_1 ≠ 0)
• Mathlib.Tactic.FieldSimp.DenomCondition.proof L (Mathlib.Tactic.FieldSimp.DenomCondition.positive iM' iM'' iM''' iM'''') = Q(0 < Mathlib.Tactic.FieldSimp.NF.eval unknown_1)

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

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`

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, 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.

Equations

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

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

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.

Equations

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

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

The goal of the simprocs grouped under the field attribute is to clear denominators in (semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then cross-multiplying. For example, the field simproc 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
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

The field simproc-set's functionality is a variant of the more general field_simp tactic, which not only clears denominators in field (in)equalities but also brings isolated field expressions into the normal form n / d (where neither n nor d contains any division symbol). (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity" side conditions. The field simproc-set 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 in the simp call (e.g. simp [field, hx]). If your (in)equality is not completely reduced by the field simproc-set, check the denominators of the resulting (in)equality and provide proofs that they are nonzero/positive to enable further progress.

Equations

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

def fieldEq : Lean.Meta.Simp.Simproc

The goal of the simprocs grouped under the field attribute is to clear denominators in (semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then cross-multiplying. For example, the field simproc 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
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

The field simproc-set's functionality is a variant of the more general field_simp tactic, which not only clears denominators in field (in)equalities but also brings isolated field expressions into the normal form n / d (where neither n nor d contains any division symbol). (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity" side conditions. The field simproc-set 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 in the simp call (e.g. simp [field, hx]). If your (in)equality is not completely reduced by the field simproc-set, check the denominators of the resulting (in)equality and provide proofs that they are nonzero/positive to enable further progress.

Equations

• fieldEq = Mathlib.Tactic.FieldSimp.proc

def fieldLe : Lean.Meta.Simp.Simproc

The goal of the simprocs grouped under the field attribute is to clear denominators in (semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then cross-multiplying. For example, the field simproc 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
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

The field simproc-set's functionality is a variant of the more general field_simp tactic, which not only clears denominators in field (in)equalities but also brings isolated field expressions into the normal form n / d (where neither n nor d contains any division symbol). (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity" side conditions. The field simproc-set 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 in the simp call (e.g. simp [field, hx]). If your (in)equality is not completely reduced by the field simproc-set, check the denominators of the resulting (in)equality and provide proofs that they are nonzero/positive to enable further progress.

Equations

• fieldLe = Mathlib.Tactic.FieldSimp.proc

def fieldLt : Lean.Meta.Simp.Simproc

The goal of the simprocs grouped under the field attribute is to clear denominators in (semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then cross-multiplying. For example, the field simproc 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
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`

The field simproc-set's functionality is a variant of the more general field_simp tactic, which not only clears denominators in field (in)equalities but also brings isolated field expressions into the normal form n / d (where neither n nor d contains any division symbol). (For confluence reasons, the field simprocs also have a slightly different normal form from field_simp's.)

Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity" side conditions. The field simproc-set 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 in the simp call (e.g. simp [field, hx]). If your (in)equality is not completely reduced by the field simproc-set, check the denominators of the resulting (in)equality and provide proofs that they are nonzero/positive to enable further progress.

Equations

• fieldLt = Mathlib.Tactic.FieldSimp.proc

We register field_simp with the hint tactic.