Commit 2025-11-25 22:07 2f69a716

View on Github →

chore(Tactic/Ring): use Qq more honestly (#30647) This PR removes almost all uses of (q(...) : Expr) in the ring tactic implementation. This includes switching from Ring/DivisionSemiring to CommRing/Semifield, because then we can rely on assumeInstancesCommute to make Qq happy. This should not affect the generality of the ring tactic, because a Ring/DivisionSemiring that is also commutative is also a CommRing/Semifield. I wanted to do some other work on ring, but that stumbled on the fact that some q(...) proof terms weren't actually being type checked properly by Qq. This PR fixes this.

Estimated changes

Modified Mathlib/Tactic/Ring/Basic.lean

added def Mathlib.Tactic.Ring.ExBase.cast

added def Mathlib.Tactic.Ring.ExBase.cmp

added def Mathlib.Tactic.Ring.ExBase.eq

added def Mathlib.Tactic.Ring.ExProd.cast

added def Mathlib.Tactic.Ring.ExProd.cmp

added def Mathlib.Tactic.Ring.ExProd.eq

added def Mathlib.Tactic.Ring.ExSum.cast

added def Mathlib.Tactic.Ring.ExSum.cmp

added def Mathlib.Tactic.Ring.ExSum.eq

modified theorem Mathlib.Tactic.Ring.div_congr

modified theorem Mathlib.Tactic.Ring.div_pf

modified def Mathlib.Tactic.Ring.evalDiv

modified def Mathlib.Tactic.Ring.evalNeg

modified def Mathlib.Tactic.Ring.evalNegProd

modified def Mathlib.Tactic.Ring.evalZSMul

modified theorem Mathlib.Tactic.Ring.intCast_add

modified theorem Mathlib.Tactic.Ring.intCast_mul

modified theorem Mathlib.Tactic.Ring.intCast_negOfNat_Int

modified theorem Mathlib.Tactic.Ring.intCast_zero

modified theorem Mathlib.Tactic.Ring.inv_congr

modified theorem Mathlib.Tactic.Ring.inv_mul

modified theorem Mathlib.Tactic.Ring.inv_single

modified theorem Mathlib.Tactic.Ring.natCast_int

modified theorem Mathlib.Tactic.Ring.neg_add

modified theorem Mathlib.Tactic.Ring.neg_congr

modified theorem Mathlib.Tactic.Ring.neg_mul

modified theorem Mathlib.Tactic.Ring.neg_one_mul

modified theorem Mathlib.Tactic.Ring.neg_zero

modified theorem Mathlib.Tactic.Ring.smul_eq_intCast

modified theorem Mathlib.Tactic.Ring.smul_int

modified theorem Mathlib.Tactic.Ring.smul_nat

modified theorem Mathlib.Tactic.Ring.sub_congr

modified theorem Mathlib.Tactic.Ring.sub_pf

modified theorem Mathlib.Tactic.Ring.zsmul_congr