Documentation

Mathlib.Tactic.Ring.Basic

ring tactic #

A tactic for solving equations in commutative (semi)rings, where the exponents can also contain variables. Based on http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf .

More precisely, expressions of the following form are supported:

The extension to exponents means that something like 2 * 2^n * b = b * 2^(n+1) can be proved, even though it is not strictly speaking an equation in the language of commutative rings.

Implementation notes #

The basic approach to prove equalities is to normalise both sides and check for equality. The normalisation is guided by building a value in the type ExSum at the meta level, together with a proof (at the base level) that the original value is equal to the normalised version.

The outline of the file:

There are some details we glossed over which make the plan more complicated:

Caveats and future work #

The normalized form of an expression is the one that is useful for the tactic, but not as nice to read. To remedy this, the user-facing normalization calls ringNFCore.

Subtraction cancels out identical terms, but division does not. That is: a - a = 0 := by ring solves the goal, but a / a := 1 by ring doesn't. Note that 0 / 0 is generally defined to be 0, so division cancelling out is not true in general.

Multiplication of powers can be simplified a little bit further: 2 ^ n * 2 ^ n = 4 ^ n := by ring could be implemented in a similar way that 2 * a + 2 * a = 4 * a := by ring already works. This feature wasn't needed yet, so it's not implemented yet.

Tags #

ring, semiring, exponent, power

instance instOrdRat :
Equations

A shortcut instance for CommSemiring ℕ used by ring.

Equations

A typed expression of type CommSemiring ℕ used when we are working on ring subexpressions of type .

Equations
inductive Mathlib.Tactic.Ring.ExBase {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} :
Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)Qq.QQ αType
  • An atomic expression e with id id.

    Atomic expressions are those which ring cannot parse any further. For instance, a + (a % b) has a and (a % b) as atoms. The ring1 tactic does not normalize the subexpressions in atoms, but ring_nf does.

    Atoms in fact represent equivalence classes of expressions, modulo definitional equality. The field index : ℕ should be a unique number for each class, while value : expr contains a representative of this class. The function resolve_atom determines the appropriate atom for a given expression.

    atom: {u : Lean.Level} → {α : Q(Type u)} → { : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.ExBase e
  • A sum of monomials.

    sum: {u : Lean.Level} → {α : Q(Type u)} → { : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.ExSum eMathlib.Tactic.Ring.ExBase e

The base e of a normalized exponent expression.

Instances For
    inductive Mathlib.Tactic.Ring.ExProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} :
    Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)Qq.QQ αType

    A monomial, which is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient.

    Instances For
      inductive Mathlib.Tactic.Ring.ExSum {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} :
      Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)Qq.QQ αType

      A polynomial expression, which is a sum of monomials.

      Instances For
        partial def Mathlib.Tactic.Ring.ExBase.eq :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase a_1Mathlib.Tactic.Ring.ExBase bBool

        Equality test for expressions. This is not a BEq instance because it is heterogeneous.

        partial def Mathlib.Tactic.Ring.ExProd.eq :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd a_1Mathlib.Tactic.Ring.ExProd bBool

        Equality test for expressions. This is not a BEq instance because it is heterogeneous.

        partial def Mathlib.Tactic.Ring.ExSum.eq :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum a_1Mathlib.Tactic.Ring.ExSum bBool

        Equality test for expressions. This is not a BEq instance because it is heterogeneous.

        partial def Mathlib.Tactic.Ring.ExBase.cmp :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase a_1Mathlib.Tactic.Ring.ExBase bOrdering

        A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

        partial def Mathlib.Tactic.Ring.ExProd.cmp :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd a_1Mathlib.Tactic.Ring.ExProd bOrdering

        A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

        partial def Mathlib.Tactic.Ring.ExSum.cmp :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum a_1Mathlib.Tactic.Ring.ExSum bOrdering

        A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

        instance Mathlib.Tactic.Ring.instInhabitedSigmaQQExBase :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExBase e)
        Equations
        instance Mathlib.Tactic.Ring.instInhabitedSigmaQQExSum :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExSum e)
        Equations
        • One or more equations did not get rendered due to their size.
        instance Mathlib.Tactic.Ring.instInhabitedSigmaQQExProd :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExProd e)
        Equations
        partial def Mathlib.Tactic.Ring.ExBase.cast :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → { : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExBase a_1(a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExBase a

        Converts ExBase sα to ExBase sβ, assuming and are defeq.

        partial def Mathlib.Tactic.Ring.ExProd.cast :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → { : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExProd a_1(a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExProd a

        Converts ExProd sα to ExProd sβ, assuming and are defeq.

        partial def Mathlib.Tactic.Ring.ExSum.cast :
        {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → { : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExSum a_1(a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExSum a

        Converts ExSum sα to ExSum sβ, assuming and are defeq.

        structure Mathlib.Tactic.Ring.Result {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (E : Qq.QQ αType) (e : Qq.QQ α) :

        The result of evaluating an (unnormalized) expression e into the type family E (one of ExSum, ExProd, ExBase) is a (normalized) element e' and a representation E e' for it, and a proof of e = e'.

        Instances For
          instance Mathlib.Tactic.Ring.instInhabitedResult :
          {a : Lean.Level} → {α : Q(Type a)} → {E : Q(«$α»)Type} → {e : Q(«$α»)} → [inst : Inhabited ((e : Q(«$α»)) × E e)] → Inhabited (Mathlib.Tactic.Ring.Result E e)
          Equations
          • Mathlib.Tactic.Ring.instInhabitedResult = match default with | { fst := e', snd := v } => { default := { expr := e', val := v, proof := default } }

          Constructs the expression corresponding to .const n. (The .const constructor does not check that the expression is correct.)

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

          Constructs the expression corresponding to .const (-n). (The .const constructor does not check that the expression is correct.)

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Tactic.Ring.ExProd.mkRat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) :
          Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)Qq.QQ (Lean.Expr.const `Int [])Qq.QQ (Lean.Expr.const `Nat [])Lean.Expr(e : Qq.QQ α) × Mathlib.Tactic.Ring.ExProd e

          Constructs the expression corresponding to .const (-n). (The .const constructor does not check that the expression is correct.)

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Tactic.Ring.ExBase.toProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)} {a : Qq.QQ α} {b : Q()} (va : Mathlib.Tactic.Ring.ExBase a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ b) :
          Mathlib.Tactic.Ring.ExProd (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) )))))) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) )))))) a) b)) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Nat.rawCast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddCommMonoidWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toAddCommMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) ))))) (Lean.Expr.lit (Lean.Literal.natVal 1)))))

          Embed an exponent (a ExBase, ExProd pair) as a ExProd by multiplying by 1.

          Equations
          def Mathlib.Tactic.Ring.ExProd.toSum {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)} {e : Qq.QQ α} (v : Mathlib.Tactic.Ring.ExProd e) :
          Mathlib.Tactic.Ring.ExSum (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HAdd.hAdd [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Distrib.toAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toDistrib [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) ))))))) e) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [u]) α) (Lean.Expr.lit (Lean.Literal.natVal 0))) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Zero.toOfNat0 [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommMonoidWithZero.toZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toCommMonoidWithZero [u]) α) ))))))

          Embed ExProd in ExSum by adding 0.

          Equations

          Get the leading coefficient of a ExProd.

          inductive Mathlib.Tactic.Ring.Overlap {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (e : Qq.QQ α) :

          Two monomials are said to "overlap" if they differ by a constant factor, in which case the constants just add. When this happens, the constant may be either zero (if the monomials cancel) or nonzero (if they add up); the zero case is handled specially.

          Instances For
            theorem Mathlib.Tactic.Ring.add_overlap_pf {R : Type u_1} [inst : CommSemiring R] {a : R} {b : R} {c : R} (x : R) (e : ) (pq_pf : a + b = c) :
            x ^ e * a + x ^ e * b = x ^ e * c
            theorem Mathlib.Tactic.Ring.add_overlap_pf_zero {R : Type u_1} [inst : CommSemiring R] {a : R} {b : R} (x : R) (e : ) :
            def Mathlib.Tactic.Ring.evalAddOverlap {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExProd a) (vb : Mathlib.Tactic.Ring.ExProd b) :
            Option (Mathlib.Tactic.Ring.Overlap (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HAdd.hAdd [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Distrib.toAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toDistrib [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) ))))))) a) b)))

            Given monomials va, vb, attempts to add them together to get another monomial. If the monomials are not compatible, returns none. For example, xy + 2xy = 3xy is a .nonzero overlap, while xy + xz returns none and xy + -xy = 0 is a .zero overlap.

            theorem Mathlib.Tactic.Ring.add_pf_zero_add {R : Type u_1} [inst : CommSemiring R] (b : R) :
            0 + b = b
            theorem Mathlib.Tactic.Ring.add_pf_add_zero {R : Type u_1} [inst : CommSemiring R] (a : R) :
            a + 0 = a
            theorem Mathlib.Tactic.Ring.add_pf_add_overlap {R : Type u_1} [inst : CommSemiring R] {a₁ : R} {b₁ : R} {c₁ : R} {a₂ : R} {b₂ : R} {c₂ : R} :
            a₁ + b₁ = c₁a₂ + b₂ = c₂a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
            theorem Mathlib.Tactic.Ring.add_pf_add_overlap_zero {R : Type u_1} [inst : CommSemiring R] {a₁ : R} {b₁ : R} {a₂ : R} {b₂ : R} {c : R} (h : Mathlib.Meta.NormNum.IsNat (a₁ + b₁) 0) (h₄ : a₂ + b₂ = c) :
            a₁ + a₂ + (b₁ + b₂) = c
            theorem Mathlib.Tactic.Ring.add_pf_add_lt {R : Type u_1} [inst : CommSemiring R] {a₂ : R} {b : R} {c : R} (a₁ : R) :
            a₂ + b = ca₁ + a₂ + b = a₁ + c
            theorem Mathlib.Tactic.Ring.add_pf_add_gt {R : Type u_1} [inst : CommSemiring R] {a : R} {b₂ : R} {c : R} (b₁ : R) :
            a + b₂ = ca + (b₁ + b₂) = b₁ + c
            partial def Mathlib.Tactic.Ring.evalAdd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExSum b) :
            Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum ) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HAdd.hAdd [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Distrib.toAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toDistrib [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) ))))))) a) b))

            Adds two polynomials va, vb together to get a normalized result polynomial.

            • 0 + b = 0
            • a + 0 = 0
            • a * x + a * y = a * (x + y) (for x, y coefficients; uses evalAddOverlap)
            • (a₁ + a₂) + (b₁ + b₂) = a₁ + (a₂ + (b₁ + b₂)) (if a₁.lt b₁)
            • (a₁ + a₂) + (b₁ + b₂) = b₁ + ((a₁ + a₂) + b₂) (if not a₁.lt b₁)
            theorem Mathlib.Tactic.Ring.one_mul {R : Type u_1} [inst : CommSemiring R] (a : R) :
            theorem Mathlib.Tactic.Ring.mul_one {R : Type u_1} [inst : CommSemiring R] (a : R) :
            theorem Mathlib.Tactic.Ring.mul_pf_left {R : Type u_1} [inst : CommSemiring R] {a₃ : R} {b : R} {c : R} (a₁ : R) (a₂ : ) :
            a₃ * b = ca₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c
            theorem Mathlib.Tactic.Ring.mul_pf_right {R : Type u_1} [inst : CommSemiring R] {a : R} {b₃ : R} {c : R} (b₁ : R) (b₂ : ) :
            a * b₃ = ca * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c
            theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap {R : Type u_1} [inst : CommSemiring R] {ea : } {eb : } {e : } {a₂ : R} {b₂ : R} {c : R} (x : R) :
            ea + eb = ea₂ * b₂ = cx ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
            partial def Mathlib.Tactic.Ring.evalMulProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExProd a) (vb : Mathlib.Tactic.Ring.ExProd b) :
            Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd ) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) )))))) a) b))

            Multiplies two monomials va, vb together to get a normalized result monomial.

            • x * y = (x * y) (for x, y coefficients)
            • x * (b₁ * b₂) = b₁ * (b₂ * x) (for x coefficient)
            • (a₁ * a₂) * y = a₁ * (a₂ * y) (for y coefficient)
            • (x ^ ea * a₂) * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂) (if ea and eb are identical except coefficient)
            • (a₁ * a₂) * (b₁ * b₂) = a₁ * (a₂ * (b₁ * b₂)) (if a₁.lt b₁)
            • (a₁ * a₂) * (b₁ * b₂) = b₁ * ((a₁ * a₂) * b₂) (if not a₁.lt b₁)
            theorem Mathlib.Tactic.Ring.mul_zero {R : Type u_1} [inst : CommSemiring R] (a : R) :
            a * 0 = 0
            theorem Mathlib.Tactic.Ring.mul_add {R : Type u_1} [inst : CommSemiring R] {a : R} {b₁ : R} {c₁ : R} {b₂ : R} {c₂ : R} {d : R} :
            a * b₁ = c₁a * b₂ = c₂c₁ + 0 + c₂ = da * (b₁ + b₂) = d
            def Mathlib.Tactic.Ring.evalMul₁ {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExProd a) (vb : Mathlib.Tactic.Ring.ExSum b) :
            Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum ) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) )))))) a) b))

            Multiplies a monomial va to a polynomial vb to get a normalized result polynomial.

            • a * 0 = 0
            • a * (b₁ + b₂) = (a * b₁) + (a * b₂)
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.Ring.zero_mul {R : Type u_1} [inst : CommSemiring R] (b : R) :
            0 * b = 0
            theorem Mathlib.Tactic.Ring.add_mul {R : Type u_1} [inst : CommSemiring R] {a₁ : R} {b : R} {c₁ : R} {a₂ : R} {c₂ : R} {d : R} :
            a₁ * b = c₁a₂ * b = c₂c₁ + c₂ = d(a₁ + a₂) * b = d
            def Mathlib.Tactic.Ring.evalMul {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExSum b) :
            Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum ) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) )))))) a) b))

            Multiplies two polynomials va, vb together to get a normalized result polynomial.

            • 0 * b = 0
            • (a₁ + a₂) * b = (a₁ * b) + (a₂ * b)
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.Ring.natCast_mul {R : Type u_1} [inst : CommSemiring R] {a₁ : } {b₁ : R} {a₃ : } {b₃ : R} (a₂ : ) :
            a₁ = b₁a₃ = b₃↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
            theorem Mathlib.Tactic.Ring.natCast_zero {R : Type u_1} [inst : CommSemiring R] :
            0 = 0
            theorem Mathlib.Tactic.Ring.natCast_add {R : Type u_1} [inst : CommSemiring R] {a₁ : } {b₁ : R} {a₂ : } {b₂ : R} :
            a₁ = b₁a₂ = b₂↑(a₁ + a₂) = b₁ + b₂

            Applies Nat.cast to a nat polynomial to produce a polynomial in α.

            • An atom e causes ↑e↑e to be allocated as a new atom.
            • A sum delegates to ExSum.evalNatCast.

            Applies Nat.cast to a nat monomial to produce a monomial in α.

            • ↑c = c↑c = c if c is a numeric literal
            • ↑(a ^ n * b) = ↑a ^ n * ↑b↑(a ^ n * b) = ↑a ^ n * ↑b↑a ^ n * ↑b↑b

            Applies Nat.cast to a nat polynomial to produce a polynomial in α.

            • ↑0 = 0↑0 = 0
            • ↑(a + b) = ↑a + ↑b↑(a + b) = ↑a + ↑b↑a + ↑b↑b
            theorem Mathlib.Tactic.Ring.smul_nat {a : } {b : } {c : } :
            a * b = ca b = c
            theorem Mathlib.Tactic.Ring.smul_eq_cast {R : Type u_1} [inst : CommSemiring R] {a : } {a' : R} {b : R} {c : R} :
            a = a'a' * b = ca b = c
            def Mathlib.Tactic.Ring.evalNSMul {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Q()} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExSum Mathlib.Tactic.Ring.sℕ a) (vb : Mathlib.Tactic.Ring.ExSum b) :
            Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum ) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HSMul.hSMul [Lean.Level.zero, u, u]) (Lean.Expr.const `Nat [])) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHSMul [Lean.Level.zero, u]) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddMonoid.SMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne.toAddMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddCommMonoidWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toAddCommMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) )))))))) a) b)))

            Constructs the scalar multiplication n • a, where both n : ℕ and a : α are normalized polynomial expressions.

            • a • b = a * b if α = ℕ
            • a • b = ↑a * b↑a * b otherwise
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.Ring.neg_one_mul {R : Type u_1} [inst : Ring R] {a : R} {b : R} :
            Int.rawCast (Int.negOfNat 1) * a = b-a = b
            theorem Mathlib.Tactic.Ring.neg_mul {R : Type u_1} [inst : Ring R] (a₁ : R) (a₂ : ) {a₃ : R} {b : R} :
            -a₃ = b-(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

            Negates a monomial va to get another monomial.

            • -c = (-c) (for c coefficient)
            • -(a₁ * a₂) = a₁ * -a₂
            theorem Mathlib.Tactic.Ring.neg_zero {R : Type u_1} [inst : Ring R] :
            -0 = 0
            theorem Mathlib.Tactic.Ring.neg_add {R : Type u_1} [inst : Ring R] {a₁ : R} {a₂ : R} {b₁ : R} {b₂ : R} :
            -a₁ = b₁-a₂ = b₂-(a₁ + a₂) = b₁ + b₂

            Negates a polynomial va to get another polynomial.

            • -0 = 0 (for c coefficient)
            • -(a₁ + a₂) = -a₁ + -a₂
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.Ring.sub_pf {R : Type u_1} [inst : Ring R] {a : R} {b : R} {c : R} {d : R} :
            -b = ca + c = da - b = d

            Subtracts two polynomials va, vb to get a normalized result polynomial.

            • a - b = a + -b
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.Ring.pow_prod_atom {R : Type u_1} [inst : CommSemiring R] (a : R) (b : ) :
            a ^ b = (a + 0) ^ b * Nat.rawCast 1

            The fallback case for exponentiating polynomials is to use ExBase.toProd to just build an exponent expression. (This has a slightly different normalization than evalPowAtom because the input types are different.)

            • x ^ e = (x + 0) ^ e * 1
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.Ring.pow_atom {R : Type u_1} [inst : CommSemiring R] (a : R) (b : ) :
            a ^ b = a ^ b * Nat.rawCast 1 + 0

            The fallback case for exponentiating polynomials is to use ExBase.toProd to just build an exponent expression.

            • x ^ e = x ^ e * 1 + 0
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.Ring.mul_exp_pos {a₁ : } {a₂ : } (n : ) (h₁ : 0 < a₁) (h₂ : 0 < a₂) :
            0 < a₁ ^ n * a₂
            theorem Mathlib.Tactic.Ring.add_pos_left {a₁ : } (a₂ : ) (h : 0 < a₁) :
            0 < a₁ + a₂
            theorem Mathlib.Tactic.Ring.add_pos_right {a₂ : } (a₁ : ) (h : 0 < a₂) :
            0 < a₁ + a₂

            Attempts to prove that a polynomial expression in is positive.

            • Atoms are not (necessarily) positive
            • Sums defer to ExSum.evalPos

            Attempts to prove that a monomial expression in is positive.

            • 0 < c (where c is a numeral) is true by the normalization invariant (c is not zero)
            • 0 < x ^ e * b if 0 < x and 0 < b

            Attempts to prove that a polynomial expression in is positive.

            • 0 < 0 fails
            • 0 < a + b if 0 < a or 0 < b
            theorem Mathlib.Tactic.Ring.pow_one {R : Type u_1} [inst : CommSemiring R] (a : R) :
            a ^ 1 = a
            theorem Mathlib.Tactic.Ring.pow_bit0 {R : Type u_1} [inst : CommSemiring R] {a : R} {k : } {b : R} {c : R} :
            a ^ k = bb * b = ca ^ Nat.mul 2 k = c
            theorem Mathlib.Tactic.Ring.pow_bit1 {R : Type u_1} [inst : CommSemiring R] {a : R} {k : } {b : R} {c : R} {d : R} :
            a ^ k = bb * b = cc * a = da ^ Nat.add (Nat.mul 2 k) 1 = d

            The main case of exponentiation of ring expressions is when va is a polynomial and n is a nonzero literal expression, like (x + y)^5. In this case we work out the polynomial completely into a sum of monomials.

            • x ^ 1 = x
            • x ^ (2*n) = x ^ n * x ^ n
            • x ^ (2*n+1) = x ^ n * x ^ n * x
            theorem Mathlib.Tactic.Ring.mul_pow {R : Type u_1} [inst : CommSemiring R] {ea₁ : } {b : } {c₁ : } {a₂ : R} {c₂ : R} {xa₁ : R} :
            ea₁ * b = c₁a₂ ^ b = c₂(xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

            There are several special cases when exponentiating monomials:

            • 1 ^ n = 1
            • x ^ y = (x ^ y) when x and y are constants
            • (a * b) ^ e = a ^ e * b ^ e

            In all other cases we use evalPowProdAtom.

            The result of extractCoeff is a numeral and a proof that the original expression factors by this numeral.

            Instances For
              theorem Mathlib.Tactic.Ring.coeff_mul {a₃ : } {c₂ : } {k : } (a₁ : ) (a₂ : ) :
              a₃ = c₂ * ka₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k

              Given a monomial expression va, splits off the leading coefficient k and the remainder e', stored in the ExtractCoeff structure.

              • c = 1 * c (if c is a constant)
              • a * b = (a * b') * k if b = b' * k
              theorem Mathlib.Tactic.Ring.pow_one_cast {R : Type u_1} [inst : CommSemiring R] (a : R) :
              theorem Mathlib.Tactic.Ring.zero_pow {R : Type u_1} [inst : CommSemiring R] {b : } :
              0 < b0 ^ b = 0
              theorem Mathlib.Tactic.Ring.single_pow {R : Type u_1} [inst : CommSemiring R] {a : R} {b : } {c : R} :
              a ^ b = c(a + 0) ^ b = c + 0
              theorem Mathlib.Tactic.Ring.pow_nat {R : Type u_1} [inst : CommSemiring R] {b : } {c : } {k : } {a : R} {d : R} {e : R} :
              b = c * ka ^ c = dd ^ k = ea ^ b = e

              Exponentiates a polynomial va by a monomial vb, including several special cases.

              • a ^ 1 = a
              • 0 ^ e = 0 if 0 < e
              • (a + 0) ^ b = a ^ b computed using evalPowProd
              • a ^ b = (a ^ b') ^ k if b = b' * k and k > 1

              Otherwise a ^ b is just encoded as a ^ b * 1 + 0 using evalPowAtom.

              theorem Mathlib.Tactic.Ring.pow_zero {R : Type u_1} [inst : CommSemiring R] (a : R) :
              a ^ 0 = Nat.rawCast 1 + 0
              theorem Mathlib.Tactic.Ring.pow_add {R : Type u_1} [inst : CommSemiring R] {a : R} {b₁ : } {c₁ : R} {b₂ : } {c₂ : R} {d : R} :
              a ^ b₁ = c₁a ^ b₂ = c₂c₁ * c₂ = da ^ (b₁ + b₂) = d

              Exponentiates two polynomials va, vb.

              • a ^ 0 = 1
              • a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
              Equations
              • One or more equations did not get rendered due to their size.
              structure Mathlib.Tactic.Ring.Cache {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) :

              This cache contains data required by the ring tactic during execution.

              Instances For

                Create a new cache for α by doing the necessary instance searches.

                Equations
                • One or more equations did not get rendered due to their size.
                theorem Mathlib.Tactic.Ring.cast_pos {R : Type u_1} [inst : CommSemiring R] {a : R} {n : } :
                theorem Mathlib.Tactic.Ring.cast_zero {R : Type u_1} [inst : CommSemiring R] {a : R} :
                theorem Mathlib.Tactic.Ring.cast_rat {n : } {d : } {R : Type u_1} [inst : DivisionRing R] {a : R} :

                Converts a proof by norm_num that e is a numeral, into a normalization as a monomial:

                • e = 0 if norm_num returns IsNat e 0
                • e = Nat.rawCast n + 0 if norm_num returns IsNat e n
                • e = Int.rawCast n + 0 if norm_num returns IsInt e n
                • e = Rat.rawCast n d + 0 if norm_num returns IsRat e n d
                Equations
                • One or more equations did not get rendered due to their size.
                theorem Mathlib.Tactic.Ring.toProd_pf {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} (p : a = a') :
                theorem Mathlib.Tactic.Ring.atom_pf {R : Type u_1} [inst : CommSemiring R] (a : R) :
                theorem Mathlib.Tactic.Ring.atom_pf' {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} (p : a = a') :

                Evaluates an atom, an expression where ring can find no additional structure.

                • a = a ^ 1 * 1 + 0
                Equations
                • One or more equations did not get rendered due to their size.
                theorem Mathlib.Tactic.Ring.inv_mul {R : Type u_1} [inst : DivisionRing R] {a₁ : R} {a₂ : } {a₃ : R} {b₁ : R} {b₃ : R} {c : R} :
                a₁⁻¹ = b₁a₃⁻¹ = b₃b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c(a₁ ^ a₂ * a₃)⁻¹ = c
                theorem Mathlib.Tactic.Ring.inv_single {R : Type u_1} [inst : DivisionRing R] {a : R} {b : R} :
                a⁻¹ = b(a + 0)⁻¹ = b + 0
                theorem Mathlib.Tactic.Ring.inv_add {R : Type u_1} [inst : CommSemiring R] {a₁ : } {b₁ : R} {a₂ : } {b₂ : R} :
                a₁ = b₁a₂ = b₂↑(a₁ + a₂) = b₁ + b₂

                Applies ⁻¹⁻¹ to a polynomial to get an atom.

                Equations
                • One or more equations did not get rendered due to their size.
                def Mathlib.Tactic.Ring.ExProd.evalInv {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (dα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) {a : Qq.QQ α} (czα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) )))))) (va : Mathlib.Tactic.Ring.ExProd a) :

                Inverts a polynomial va to get a normalized result polynomial.

                • c⁻¹ = (c⁻¹)⁻¹ = (c⁻¹)⁻¹) if c is a constant
                • (a ^ b * c)⁻¹ = a⁻¹ ^ b * c⁻¹⁻¹ = a⁻¹ ^ b * c⁻¹⁻¹ ^ b * c⁻¹⁻¹
                def Mathlib.Tactic.Ring.ExSum.evalInv {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (dα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) {a : Qq.QQ α} (czα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) )))))) (va : Mathlib.Tactic.Ring.ExSum a) :

                Inverts a polynomial va to get a normalized result polynomial.

                • 0⁻¹ = 0⁻¹ = 0
                • a⁻¹ = (a⁻¹)⁻¹ = (a⁻¹)⁻¹) if a is a nontrivial sum
                Equations
                • One or more equations did not get rendered due to their size.
                theorem Mathlib.Tactic.Ring.div_pf {R : Type u_1} [inst : DivisionRing R] {a : R} {b : R} {c : R} {d : R} :
                b⁻¹ = ca * c = da / b = d
                def Mathlib.Tactic.Ring.evalDiv {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) (czα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) )))))) (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExSum b) :

                Divides two polynomials va, vb to get a normalized result polynomial.

                • a / b = a * b⁻¹⁻¹
                Equations
                • One or more equations did not get rendered due to their size.
                theorem Mathlib.Tactic.Ring.add_congr {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                a = a'b = b'a' + b' = ca + b = c
                theorem Mathlib.Tactic.Ring.mul_congr {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                a = a'b = b'a' * b' = ca * b = c
                theorem Mathlib.Tactic.Ring.nsmul_congr {R : Type u_1} [inst : CommSemiring R] {a : } {a' : } {b : R} {b' : R} {c : R} :
                a = a'b = b'a' b' = ca b = c
                theorem Mathlib.Tactic.Ring.pow_congr {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} {b : } {b' : } {c : R} :
                a = a'b = b'a' ^ b' = ca ^ b = c
                theorem Mathlib.Tactic.Ring.neg_congr {R : Type u_1} [inst : Ring R] {a : R} {a' : R} {b : R} :
                a = a'-a' = b-a = b
                theorem Mathlib.Tactic.Ring.sub_congr {R : Type u_1} [inst : Ring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                a = a'b = b'a' - b' = ca - b = c
                theorem Mathlib.Tactic.Ring.inv_congr {R : Type u_1} [inst : DivisionRing R] {a : R} {a' : R} {b : R} :
                a = a'a'⁻¹ = ba⁻¹ = b
                theorem Mathlib.Tactic.Ring.div_congr {R : Type u_1} [inst : DivisionRing R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                a = a'b = b'a' / b' = ca / b = c

                Checks whether e would be processed by eval as a ring expression, or otherwise if it is an atom or something simplifiable via norm_num.

                We use this in ring_ng to avoid rewriting atoms unnecessarily.

                Returns:

                • none if eval would process e as an algebraic ring expression
                • some none if eval would treat e as an atom.
                • some (some r) if eval would not process e as an algebraic ring expression, but NormNum.derive can nevertheless simplify e, with result r.
                Equations
                • One or more equations did not get rendered due to their size.

                Evaluates expression e of type α into a normalized representation as a polynomial. This is the main driver of ring, which calls out to evalAdd, evalMul etc.

                theorem Mathlib.Tactic.Ring.of_eq {R : Type u_1} {a : R} {c : R} {b : R} :
                a = cb = ca = b

                This is a routine which is used to clean up the unsolved subgoal of a failed ring1 application. It is overridden in Mathlib.Tactic.Ring.RingNF to apply the ring_nf simp set to the goal.

                Frontend of ring1: attempt to close a goal g, assuming it is an equation of semirings.

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

                Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

                • This version of ring fails if the target is not an equality.
                • The variant ring1! will use a more aggressive reducibility setting to determine equality of atoms.
                Equations
                • One or more equations did not get rendered due to their size.

                Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

                • This version of ring fails if the target is not an equality.
                • The variant ring1! will use a more aggressive reducibility setting to determine equality of atoms.
                Equations