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:

• constants (non-negative integers)
• variables
• coefficients (any rational number, embedded into the (semi)ring)
• addition of expressions
• multiplication of expressions (a * b)
• scalar multiplication of expressions (n • a; the multiplier must have type ℕ)
• exponentiation of expressions (the exponent must have type ℕ)
• subtraction and negation of expressions (if the base is a full ring)

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:

• Define a mutual inductive family of types ExSum, ExProd, ExBase, which can represent expressions with +, *, ^ and rational numerals. The mutual induction ensures that associativity and distributivity are applied, by restricting which kinds of subexpressions appear as arguments to the various operators.
• Represent addition, multiplication and exponentiation in the ExSum type, thus allowing us to map expressions to ExSum (the eval function drives this). We apply associativity and distributivity of the operators here (helped by Ex* types) and commutativity as well (by sorting the subterms; unfortunately not helped by anything). Any expression not of the above formats is treated as an atom (the same as a variable).

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

• The order on atoms is not initially obvious. We construct a list containing them in order of initial appearance in the expression, then use the index into the list as a key to order on.
• For pow, the exponent must be a natural number, while the base can be any semiring α. We swap out operations for the base ring α with those for the exponent ring ℕ as soon as we deal with exponents.

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

def Mathlib.Tactic.Ring.instCommSemiringNat : CommSemiring ℕ

A shortcut instance for CommSemiring ℕ used by ring.

Equations

• Mathlib.Tactic.Ring.instCommSemiringNat = inferInstance

def Mathlib.Tactic.Ring.sℕ : Q(CommSemiring ℕ)

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

Equations

• Mathlib.Tactic.Ring.sℕ = q(Mathlib.Tactic.Ring.instCommSemiringNat)

partial def Mathlib.Tactic.Ring.ExBase.eq : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase sα a_1 → Mathlib.Tactic.Ring.ExBase sα b → Bool

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)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd sα a_1 → Mathlib.Tactic.Ring.ExProd sα b → Bool

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)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum sα a_1 → Mathlib.Tactic.Ring.ExSum sα b → Bool

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)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase sα a_1 → Mathlib.Tactic.Ring.ExBase sα b → Ordering

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)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd sα a_1 → Mathlib.Tactic.Ring.ExProd sα b → Ordering

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)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum sα a_1 → Mathlib.Tactic.Ring.ExSum sα b → Ordering

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

instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExBase : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExBase sα e)

Equations

• Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExBase = { default := { fst := default, snd := Mathlib.Tactic.Ring.ExBase.atom 0 } }

instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExSum : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExSum sα e)

instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExProd : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExProd sα e)

Equations

• Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExProd = { default := { fst := default, snd := Mathlib.Tactic.Ring.ExProd.const 0 } }

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

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

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

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

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

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

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)

theorem Mathlib.Tactic.Ring.add_overlap_pf {R : Type u_1} [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} [CommSemiring R] {a : R} {b : R} (x : R) (e : ℕ) : Mathlib.Meta.NormNum.IsNat (a + b) 0 → Mathlib.Meta.NormNum.IsNat (x ^ e * a + x ^ e * b) 0

theorem Mathlib.Tactic.Ring.add_pf_zero_add {R : Type u_1} [CommSemiring R] (b : R) : 0 + b = b

theorem Mathlib.Tactic.Ring.add_pf_add_zero {R : Type u_1} [CommSemiring R] (a : R) : a + 0 = a

theorem Mathlib.Tactic.Ring.add_pf_add_overlap {R : Type u_1} [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} [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} [CommSemiring R] {a₂ : R} {b : R} {c : R} (a₁ : R) : a₂ + b = c → a₁ + a₂ + b = a₁ + c

theorem Mathlib.Tactic.Ring.add_pf_add_gt {R : Type u_1} [CommSemiring R] {a : R} {b₂ : R} {c : R} (b₁ : R) : a + b₂ = c → a + (b₁ + b₂) = b₁ + c

theorem Mathlib.Tactic.Ring.one_mul {R : Type u_1} [CommSemiring R] (a : R) : Nat.rawCast 1 * a = a

theorem Mathlib.Tactic.Ring.mul_one {R : Type u_1} [CommSemiring R] (a : R) : a * Nat.rawCast 1 = a

theorem Mathlib.Tactic.Ring.mul_pf_left {R : Type u_1} [CommSemiring R] {a₃ : R} {b : R} {c : R} (a₁ : R) (a₂ : ℕ) : a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

theorem Mathlib.Tactic.Ring.mul_pf_right {R : Type u_1} [CommSemiring R] {a : R} {b₃ : R} {c : R} (b₁ : R) (b₂ : ℕ) : a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap {R : Type u_1} [CommSemiring R] {ea : ℕ} {eb : ℕ} {e : ℕ} {a₂ : R} {b₂ : R} {c : R} (x : R) : ea + eb = e → a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

theorem Mathlib.Tactic.Ring.mul_zero {R : Type u_1} [CommSemiring R] (a : R) : a * 0 = 0

theorem Mathlib.Tactic.Ring.mul_add {R : Type u_1} [CommSemiring R] {a : R} {b₁ : R} {c₁ : R} {b₂ : R} {c₂ : R} {d : R} : a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d

theorem Mathlib.Tactic.Ring.zero_mul {R : Type u_1} [CommSemiring R] (b : R) : 0 * b = 0

theorem Mathlib.Tactic.Ring.add_mul {R : Type u_1} [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

theorem Mathlib.Tactic.Ring.natCast_nat {R : Type u_1} [CommSemiring R] (n : ℕ) : ↑(Nat.rawCast n) = Nat.rawCast n

theorem Mathlib.Tactic.Ring.natCast_mul {R : Type u_1} [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} [CommSemiring R] : ↑0 = 0

theorem Mathlib.Tactic.Ring.natCast_add {R : Type u_1} [CommSemiring R] {a₁ : ℕ} {b₁ : R} {a₂ : ℕ} {b₂ : R} : ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂

theorem Mathlib.Tactic.Ring.smul_nat {a : ℕ} {b : ℕ} {c : ℕ} : a * b = c → a • b = c

theorem Mathlib.Tactic.Ring.smul_eq_cast {R : Type u_1} [CommSemiring R] {a : ℕ} {a' : R} {b : R} {c : R} : ↑a = a' → a' * b = c → a • b = c

theorem Mathlib.Tactic.Ring.neg_one_mul {R : Type u_1} [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} [Ring R] (a₁ : R) (a₂ : ℕ) {a₃ : R} {b : R} : -a₃ = b → -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

theorem Mathlib.Tactic.Ring.neg_zero {R : Type u_1} [Ring R] : -0 = 0

theorem Mathlib.Tactic.Ring.neg_add {R : Type u_1} [Ring R] {a₁ : R} {a₂ : R} {b₁ : R} {b₂ : R} : -a₁ = b₁ → -a₂ = b₂ → -(a₁ + a₂) = b₁ + b₂

theorem Mathlib.Tactic.Ring.sub_pf {R : Type u_1} [Ring R] {a : R} {b : R} {c : R} {d : R} : -b = c → a + c = d → a - b = d

theorem Mathlib.Tactic.Ring.pow_prod_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ℕ) : a ^ b = (a + 0) ^ b * Nat.rawCast 1

theorem Mathlib.Tactic.Ring.pow_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ℕ) : a ^ b = a ^ b * Nat.rawCast 1 + 0

theorem Mathlib.Tactic.Ring.const_pos (n : ℕ) (h : Nat.ble 1 n = true) : 0 < Nat.rawCast n

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₂

theorem Mathlib.Tactic.Ring.pow_one {R : Type u_1} [CommSemiring R] (a : R) : a ^ 1 = a

theorem Mathlib.Tactic.Ring.pow_bit0 {R : Type u_1} [CommSemiring R] {a : R} {k : ℕ} {b : R} {c : R} : a ^ k = b → b * b = c → a ^ Nat.mul 2 k = c

theorem Mathlib.Tactic.Ring.pow_bit1 {R : Type u_1} [CommSemiring R] {a : R} {k : ℕ} {b : R} {c : R} {d : R} : a ^ k = b → b * b = c → c * a = d → a ^ Nat.add (Nat.mul 2 k) 1 = d

theorem Mathlib.Tactic.Ring.one_pow {R : Type u_1} [CommSemiring R] (b : ℕ) : Nat.rawCast 1 ^ b = Nat.rawCast 1

theorem Mathlib.Tactic.Ring.mul_pow {R : Type u_1} [CommSemiring R] {ea₁ : ℕ} {b : ℕ} {c₁ : ℕ} {a₂ : R} {c₂ : R} {xa₁ : R} : ea₁ * b = c₁ → a₂ ^ b = c₂ → (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

structure Mathlib.Tactic.Ring.ExtractCoeff (e : Q(ℕ)) : Type

• k : Q(ℕ)

  A raw natural number literal.

• e' : Q(ℕ)

  The result of extracting the coefficient is a monic monomial.

• ve' : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ s.e'

  e' is a monomial.

• p : Q(«$e» = unknown_1 * unknown_2)

  The proof that e splits into the coefficient k and the monic monomial e'.

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

theorem Mathlib.Tactic.Ring.coeff_one (k : ℕ) : Nat.rawCast k = Nat.rawCast 1 * k

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

def Mathlib.Tactic.Ring.extractCoeff {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ a) : Mathlib.Tactic.Ring.ExtractCoeff a

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} [CommSemiring R] (a : R) : a ^ Nat.rawCast 1 = a

theorem Mathlib.Tactic.Ring.zero_pow {R : Type u_1} [CommSemiring R] {b : ℕ} : 0 < b → 0 ^ b = 0

theorem Mathlib.Tactic.Ring.single_pow {R : Type u_1} [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} [CommSemiring R] {b : ℕ} {c : ℕ} {k : ℕ} {a : R} {d : R} {e : R} : b = c * k → a ^ c = d → d ^ k = e → a ^ b = e

theorem Mathlib.Tactic.Ring.pow_zero {R : Type u_1} [CommSemiring R] (a : R) : a ^ 0 = Nat.rawCast 1 + 0

theorem Mathlib.Tactic.Ring.pow_add {R : Type u_1} [CommSemiring R] {a : R} {b₁ : ℕ} {c₁ : R} {b₂ : ℕ} {c₂ : R} {d : R} : a ^ b₁ = c₁ → a ^ b₂ = c₂ → c₁ * c₂ = d → a ^ (b₁ + b₂) = d

theorem Mathlib.Tactic.Ring.cast_pos {R : Type u_1} [CommSemiring R] {a : R} {n : ℕ} : Mathlib.Meta.NormNum.IsNat a n → a = Nat.rawCast n + 0

theorem Mathlib.Tactic.Ring.cast_zero {R : Type u_1} [CommSemiring R] {a : R} : Mathlib.Meta.NormNum.IsNat a 0 → a = 0

theorem Mathlib.Tactic.Ring.cast_neg {n : ℕ} {R : Type u_1} [Ring R] {a : R} : Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → a = Int.rawCast (Int.negOfNat n) + 0

theorem Mathlib.Tactic.Ring.cast_rat {n : ℤ} {d : ℕ} {R : Type u_1} [DivisionRing R] {a : R} : Mathlib.Meta.NormNum.IsRat a n d → a = Rat.rawCast n d + 0

theorem Mathlib.Tactic.Ring.toProd_pf {R : Type u_1} [CommSemiring R] {a : R} {a' : R} (p : a = a') : a = a' ^ Nat.rawCast 1 * Nat.rawCast 1

theorem Mathlib.Tactic.Ring.atom_pf {R : Type u_1} [CommSemiring R] (a : R) : a = a ^ Nat.rawCast 1 * Nat.rawCast 1 + 0

theorem Mathlib.Tactic.Ring.atom_pf' {R : Type u_1} [CommSemiring R] {a : R} {a' : R} (p : a = a') : a = a' ^ Nat.rawCast 1 * Nat.rawCast 1 + 0

theorem Mathlib.Tactic.Ring.inv_mul {R : Type u_1} [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_zero {R : Type u_1} [DivisionRing R] : 0⁻¹ = 0

theorem Mathlib.Tactic.Ring.inv_single {R : Type u_1} [DivisionRing R] {a : R} {b : R} : a⁻¹ = b → (a + 0)⁻¹ = b + 0

theorem Mathlib.Tactic.Ring.inv_add {R : Type u_1} [CommSemiring R] {a₁ : ℕ} {b₁ : R} {a₂ : ℕ} {b₂ : R} : ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂

theorem Mathlib.Tactic.Ring.div_pf {R : Type u_1} [DivisionRing R] {a : R} {b : R} {c : R} {d : R} : b⁻¹ = c → a * c = d → a / b = d

theorem Mathlib.Tactic.Ring.add_congr {R : Type u_1} [CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' + b' = c → a + b = c

theorem Mathlib.Tactic.Ring.mul_congr {R : Type u_1} [CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' * b' = c → a * b = c

theorem Mathlib.Tactic.Ring.nsmul_congr {R : Type u_1} [CommSemiring R] {a : ℕ} {a' : ℕ} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' • b' = c → a • b = c

theorem Mathlib.Tactic.Ring.pow_congr {R : Type u_1} [CommSemiring R] {a : R} {a' : R} {b : ℕ} {b' : ℕ} {c : R} : a = a' → b = b' → a' ^ b' = c → a ^ b = c

theorem Mathlib.Tactic.Ring.neg_congr {R : Type u_1} [Ring R] {a : R} {a' : R} {b : R} : a = a' → -a' = b → -a = b

theorem Mathlib.Tactic.Ring.sub_congr {R : Type u_1} [Ring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' - b' = c → a - b = c

theorem Mathlib.Tactic.Ring.inv_congr {R : Type u_1} [DivisionRing R] {a : R} {a' : R} {b : R} : a = a' → a'⁻¹ = b → a⁻¹ = b

theorem Mathlib.Tactic.Ring.div_congr {R : Type u_1} [DivisionRing R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' / b' = c → a / b = c

def Mathlib.Tactic.Ring.Cache.nat : Mathlib.Tactic.Ring.Cache Mathlib.Tactic.Ring.sℕ

A precomputed Cache for ℕ.

Equations

• Mathlib.Tactic.Ring.Cache.nat = { rα := none, dα := none, czα := some q((_ : CharZero ℕ)) }

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

opaque Mathlib.Tactic.Ring.ringCleanupRef : IO.Ref (Lean.Expr → Lean.MetaM Lean.Expr)

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.

def Mathlib.Tactic.Ring.proveEq (g : Lean.MVarId) : Mathlib.Tactic.AtomM Unit

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.

def Mathlib.Tactic.Ring.ring1 : Lean.ParserDescr

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.

def Mathlib.Tactic.Ring.tacticRing1! : Lean.ParserDescr

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

• Mathlib.Tactic.Ring.tacticRing1! = Lean.ParserDescr.node `Mathlib.Tactic.Ring.tacticRing1! 1024 (Lean.ParserDescr.nonReservedSymbol "ring1!" false)