∀ (a : Lean.Grind.CommRing.Power) (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power)
  (b_1 : Lean.Grind.CommRing.Mon),
  (Lean.Grind.CommRing.Mon.mult a a_1 == Lean.Grind.CommRing.Mon.mult b b_1) = (a == b && a_1 == b_1)