structure Mathlib.Tactic.RPowRing.Context : Type

The read-only state of the RPowRing monad.

• ctx : Lean.Meta.Simp.Context

  A basically empty simp context, passed to the simp traversal in RPowRing.rewrite.

• simp : Lean.Meta.Simp.Result → Lean.Meta.SimpM Lean.Meta.Simp.Result

  A cleanup routine, which simplifies normalized polynomials to a more human-friendly format.

structure Mathlib.Tactic.RPowRing.Config : Type

Configuration for ring_nf.

• red : Lean.Meta.TransparencyMode

  the reducibility setting to use when comparing atoms for defeq

instance Mathlib.Tactic.RPowRing.instInhabitedConfig : Inhabited Mathlib.Tactic.RPowRing.Config

Equations

• Mathlib.Tactic.RPowRing.instInhabitedConfig = { default := { red := default } }

instance Mathlib.Tactic.RPowRing.instBEqConfig : BEq Mathlib.Tactic.RPowRing.Config

Equations

• Mathlib.Tactic.RPowRing.instBEqConfig = { beq := Mathlib.Tactic.RPowRing.beqConfig✝ }

instance Mathlib.Tactic.RPowRing.instReprConfig : Repr Mathlib.Tactic.RPowRing.Config

Equations

• Mathlib.Tactic.RPowRing.instReprConfig = { reprPrec := Mathlib.Tactic.RPowRing.reprConfig✝ }

def Mathlib.Tactic.RPowRing.elabConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Mathlib.Tactic.RPowRing.Config

Function elaborating RingNF.Config.

Equations

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

@[reducible, inline]

abbrev Mathlib.Tactic.RPowRing.M (α : Type) : Type

The monad for RingNF contains, in addition to the AtomM state, a simp context for the main traversal and a simp function (which has another simp context) to simplify normalized polynomials.

Equations

• Mathlib.Tactic.RPowRing.M = ReaderT Mathlib.Tactic.RPowRing.Context Mathlib.Tactic.AtomM

inductive Mathlib.Tactic.RPowRing.ExBase (e : Q(ℝ)) : Type

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

• atom: ℕ → (x : Q(ℝ)) → Mathlib.Tactic.RPowRing.ExBase x

  A coefficient value, which must not be 0. e is a raw rat cast. If value is not an integer, then hyp should be a proof of (value.den : α) ≠ 0.

• pow: ℕ → (x : Q(ℝ)) → Q(0 < «$x») → (e : Q(ℝ)) → Mathlib.Tactic.RPowRing.ExBase q(«$x» ^ «$e»)

  A product x ^ e * b is a monomial if b is a monomial. Here x is an ExBase and e is an ExBase representing a monomial expression in ℕ (it is a monomial instead of a polynomial because we eagerly normalize x ^ (a + b) = x ^ a * x ^ b.)

def Mathlib.Tactic.RPowRing.ExBase.id {e : Q(ℝ)} : Mathlib.Tactic.RPowRing.ExBase e → ℕ

Equations

• (Mathlib.Tactic.RPowRing.ExBase.atom id e).id = id
• (Mathlib.Tactic.RPowRing.ExBase.pow id x_1 h e_2).id = id

inductive Mathlib.Tactic.RPowRing.ExProd (e : Q(ℝ)) : Type

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

• one: Mathlib.Tactic.RPowRing.ExProd q(1)

  A coefficient value, which must not be 0. e is a raw rat cast. If value is not an integer, then hyp should be a proof of (value.den : α) ≠ 0.

• mul: {x b : Q(ℝ)} → Mathlib.Tactic.RPowRing.ExBase x → Mathlib.Tactic.RPowRing.ExProd b → Mathlib.Tactic.RPowRing.ExProd q(«$x» * «$b»)

  A product x ^ e * b is a monomial if b is a monomial. Here x is an ExBase and e is an ExProd representing a monomial expression in ℕ (it is a monomial instead of a polynomial because we eagerly normalize x ^ (a + b) = x ^ a * x ^ b.)

instance Mathlib.Tactic.RPowRing.instInhabitedSigmaQuotedConstMkStr1NilLevelExBase : Inhabited ((e : Q(ℝ)) × Mathlib.Tactic.RPowRing.ExBase e)

Equations

• Mathlib.Tactic.RPowRing.instInhabitedSigmaQuotedConstMkStr1NilLevelExBase = { default := ⟨default, Mathlib.Tactic.RPowRing.ExBase.atom 0 default⟩ }

instance Mathlib.Tactic.RPowRing.instInhabitedSigmaQuotedConstMkStr1NilLevelExProd : Inhabited ((e : Q(ℝ)) × Mathlib.Tactic.RPowRing.ExProd e)

Equations

• Mathlib.Tactic.RPowRing.instInhabitedSigmaQuotedConstMkStr1NilLevelExProd = { default := ⟨q(1), Mathlib.Tactic.RPowRing.ExProd.one⟩ }

def Mathlib.Tactic.RPowRing.ExBase.toProd {a : Q(ℝ)} (va : Mathlib.Tactic.RPowRing.ExBase a) : Mathlib.Tactic.RPowRing.ExProd q(«$a» * 1)

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

Equations

• va.toProd = Mathlib.Tactic.RPowRing.ExProd.mul va Mathlib.Tactic.RPowRing.ExProd.one

@[reducible, inline]

abbrev Mathlib.Tactic.RPowRing.Result (E : Q(ℝ) → Type) (e : Q(ℝ)) : Type

Equations

• Mathlib.Tactic.RPowRing.Result = Mathlib.Tactic.Ring.Result

instance Mathlib.Tactic.RPowRing.instInhabitedResultExProd (e : Q(ℝ)) : Inhabited (Mathlib.Tactic.RPowRing.Result Mathlib.Tactic.RPowRing.ExProd e)

Equations

• Mathlib.Tactic.RPowRing.instInhabitedResultExProd e = inferInstanceAs (Inhabited (Mathlib.Tactic.Ring.Result Mathlib.Tactic.RPowRing.ExProd e))

theorem Mathlib.Tactic.RPowRing.atom_pf (a : ℝ) : a = a * 1

theorem Mathlib.Tactic.RPowRing.atom_pf' {a : ℝ} {a' : ℝ} (p : a = a') : a = a * 1

theorem Mathlib.Tactic.RPowRing.atom_pow_pf (a : ℝ) : a = a ^ 1 * 1

theorem Mathlib.Tactic.RPowRing.atom_pow_pf' {a : ℝ} {a' : ℝ} (p : a = a') : a = a ^ 1 * 1

def Mathlib.Tactic.RPowRing.evalAtom (e : Q(ℝ)) : Mathlib.Tactic.AtomM (Mathlib.Tactic.RPowRing.Result Mathlib.Tactic.RPowRing.ExProd e)

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.RPowRing.mul_pf_left {a₂ : ℝ} {b : ℝ} {c : ℝ} (a₁ : ℝ) : a₂ * b = c → a₁ * a₂ * b = a₁ * c

theorem Mathlib.Tactic.RPowRing.mul_pf_right {a : ℝ} {b₂ : ℝ} {c : ℝ} (b₁ : ℝ) : a * b₂ = c → a * (b₁ * b₂) = b₁ * c

theorem Mathlib.Tactic.RPowRing.mul_pp_pf_overlap {a₂ : ℝ} {b₂ : ℝ} {c : ℝ} {x : ℝ} (ea : ℝ) (eb : ℝ) (h : 0 < x) : a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * c

partial def Mathlib.Tactic.RPowRing.evalMul {a : Q(ℝ)} {b : Q(ℝ)} (va : Mathlib.Tactic.RPowRing.ExProd a) (vb : Mathlib.Tactic.RPowRing.ExProd b) : Mathlib.Tactic.RPowRing.Result Mathlib.Tactic.RPowRing.ExProd q(«$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.RPowRing.pow_pos {a : ℝ} {b : ℝ} {e : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < a ^ e * b

theorem Mathlib.Tactic.RPowRing.pow_pf {a : ℝ} {b : ℝ} {b' : ℝ} {e₁ : ℝ} {e₂ : ℝ} (ha : 0 < a) (hb : 0 < b) : b ^ e₂ = b' → (a ^ e₁ * b) ^ e₂ = a ^ (e₁ * e₂) * b'

def Mathlib.Tactic.RPowRing.evalPow {a : Q(ℝ)} (va : Mathlib.Tactic.RPowRing.ExProd a) (e : Q(ℝ)) : Option (Q(0 < «$a») × Mathlib.Tactic.RPowRing.Result Mathlib.Tactic.RPowRing.ExProd q(«$a» ^ «$e»))

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.RPowRing.evalPow Mathlib.Tactic.RPowRing.ExProd.one e = some (q(⋯), { expr := q(1), val := Mathlib.Tactic.RPowRing.ExProd.one, proof := q(⋯) })
• Mathlib.Tactic.RPowRing.evalPow (Mathlib.Tactic.RPowRing.ExProd.mul (Mathlib.Tactic.RPowRing.ExBase.atom id x) vb) e = none

theorem Mathlib.Tactic.RPowRing.pow_congr {a : ℝ} {a' : ℝ} {b : ℝ} {c : ℝ} : a = a' → a' ^ b = c → a ^ b = c

theorem Mathlib.Tactic.RPowRing.inv_congr {a : ℝ} {a' : ℝ} {b : ℝ} : a = a' → a' ^ (-1) = b → a⁻¹ = b

theorem Mathlib.Tactic.RPowRing.npow_congr {a : ℝ} {a' : ℝ} {c : ℝ} {b : ℕ} : a = a' → a' ^ ↑b = c → Monoid.npow b a = c

partial def Mathlib.Tactic.RPowRing.eval (e : Q(ℝ)) : Mathlib.Tactic.AtomM (Mathlib.Tactic.RPowRing.Result Mathlib.Tactic.RPowRing.ExProd e)

def Mathlib.Tactic.RPowRing.rewrite (parent : Lean.Expr) (root : optParam Bool true) : Mathlib.Tactic.RPowRing.M Lean.Meta.Simp.Result

Equations

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

def Mathlib.Tactic.RPowRing.M.run {α : Type} (s : IO.Ref Mathlib.Tactic.AtomM.State) (cfg : Mathlib.Tactic.RPowRing.Config) (x : Mathlib.Tactic.RPowRing.M α) : Lean.MetaM α

Runs a tactic in the RingNF.M monad, given initial data:

• s: a reference to the mutable state of ring, for persisting across calls. This ensures that atom ordering is used consistently.
• cfg: the configuration options
• x: the tactic to run

Equations

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

def Mathlib.Tactic.RPowRing.rpowRingTarget (s : IO.Ref Mathlib.Tactic.AtomM.State) (cfg : Mathlib.Tactic.RPowRing.Config) : Lean.Elab.Tactic.TacticM Unit

Use rpow_ring to rewrite the main goal.

Equations

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

def Mathlib.Tactic.RPowRing.rpowRingLocalDecl (s : IO.Ref Mathlib.Tactic.AtomM.State) (cfg : Mathlib.Tactic.RPowRing.Config) (fvarId : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

Use rpow_ring to rewrite hypothesis h.

Equations

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

def Mathlib.Tactic.RPowRing.rpowRing : Lean.ParserDescr

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

• rpow_ring! will use a more aggressive reducibility setting to identify atoms.
• rpow_ring (config := cfg) allows for additional configuration:
  • red: the reducibility setting (overridden by !)
  • recursive: if true, rpow_ring will also recurse into atoms
• rpow_ring works as both a tactic and a conv tactic. In tactic mode, rpow_ring at h can be used to rewrite in a hypothesis.

Equations

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

def Mathlib.Tactic.RPowRing.tacticRpow_ring!__ : Lean.ParserDescr

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

• rpow_ring! will use a more aggressive reducibility setting to identify atoms.
• rpow_ring (config := cfg) allows for additional configuration:
  • red: the reducibility setting (overridden by !)
  • recursive: if true, rpow_ring will also recurse into atoms
• rpow_ring works as both a tactic and a conv tactic. In tactic mode, rpow_ring at h can be used to rewrite in a hypothesis.

Equations

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

def Mathlib.Tactic.RPowRing.rpowRingConv : Lean.ParserDescr

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

• rpow_ring! will use a more aggressive reducibility setting to identify atoms.
• rpow_ring (config := cfg) allows for additional configuration:
  • red: the reducibility setting (overridden by !)
  • recursive: if true, rpow_ring will also recurse into atoms
• rpow_ring works as both a tactic and a conv tactic. In tactic mode, rpow_ring at h can be used to rewrite in a hypothesis.

Equations

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

def Mathlib.Tactic.RPowRing.elabRPowRingConv : Lean.Elab.Tactic.Tactic

Elaborator for the rpow_ring tactic.

Equations

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

theorem Real.pow_neg (a : ℝ) (b : ℝ) (h : 0 ≤ a) : a ^ (-b) = a⁻¹ ^ b

theorem Real.inv_rpow' {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x⁻¹ ^ y = x ^ (-y)

theorem Real.rpow_inv {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : (x ^ y)⁻¹ = x ^ (-y)

theorem Mathlib.Tactic.RPowRing.fix_cast₁ : ↑(Int.ofNat 1) = 1

theorem Mathlib.Tactic.RPowRing.fix_cast₂ {n : ℕ} : ↑(Int.ofNat n) = ↑n

theorem Mathlib.Tactic.RPowRing.fix_cast₃ {n : ℕ} [n.AtLeastTwo] : ↑n = n

def Mathlib.Tactic.RPowRing.delab_ofNat : Lean.PrettyPrinter.Delaborator.Delab

Equations

• Mathlib.Tactic.RPowRing.delab_ofNat = Lean.PrettyPrinter.Delaborator.whenPPOption Lean.getPPNotation (Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg 1 Lean.PrettyPrinter.Delaborator.delab)

def Mathlib.Tactic.RPowRing.tacticRpow_simp__ : Lean.ParserDescr

Equations

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