def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.getMultiplier (d : PolyDerivation) : Int

Returns the multiplier k for the input polynomial. See comment at PolyDerivation.step.

structure Lean.Meta.Grind.Arith.CommRing.ProofM.State : Type

• cache : Std.HashMap UInt64 Expr
• polyDecls : Std.HashMap Poly Expr
• monDecls : Std.HashMap Mon Expr
• exprDecls : Std.HashMap RingExpr Expr
• sexprDecls : Std.HashMap SemiringExpr Expr

structure Lean.Meta.Grind.Arith.CommRing.ProofM.Context : Type

• ctx : Expr
• sctx? : Option Expr

  Context for semiring variables if available

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.ProofM (α : Type) : Type

partial def Lean.Meta.Grind.Arith.CommRing.EqCnstr.toExprProof (c : EqCnstr) : ProofM Expr

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.setUnsat (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit

Given a and b, such that a ≠ b in the core and sa and sb their reified semiring terms s.t. sa.toPoly == sb.toPoly, close the goal.

def Lean.Meta.Grind.Arith.CommRing.setNonCommRingDiseqUnsat (a b : Expr) (ra rb : RingExpr) : NonCommRingM Unit

Given a and b, such that a ≠ b in the core and ra and rb their reified ring terms s.t. ra.toPoly_nc == rb.toPoly_nc, close the goal.

def Lean.Meta.Grind.Arith.CommRing.setNonCommSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : NonCommSemiringM Unit

Given a and b, such that a ≠ b in the core and sa and sb their reified semiring terms s.t. sa.toPolyS_nc == sb.toPolyS_nc, close the goal.

def Lean.Meta.Grind.Arith.CommRing.mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr

def Lean.Meta.Grind.Arith.CommRing.mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr

def Lean.Meta.Grind.Arith.CommRing.mkEqIffProof (lhs rhs lhs' rhs' : RingExpr) : RingM Expr

def Lean.Meta.Grind.Arith.CommRing.mkTermEqProof (e e' : RingExpr) : RingM Expr

Given e and e' s.t. e.toPoly == e'.toPoly, returns a proof that e.denote ctx = e'.denote ctx

def Lean.Meta.Grind.Arith.CommRing.mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr

def Lean.Meta.Grind.Arith.CommRing.mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr

def Lean.Meta.Grind.Arith.CommRing.mkNonCommEqIffProof (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr

def Lean.Meta.Grind.Arith.CommRing.mkNonCommTermEqProof (e e' : RingExpr) : NonCommRingM Expr

Given e and e' s.t. e.toPoly_nc == e'.toPoly_nc, returns a proof that e.denote ctx = e'.denote ctx