Group Tactic for Monoids or Rings

Stream: mathlib4

[Xavier Xarles]

I am trying to prove some elementary equality for elements in a Commutative Monoid. But it happens if the elements are in a commutative rings, tactic group solves it, but for commutative monoids it does not. Moreover, you need commutativity for the equality to hold.

import Mathlib.Tactic
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.Ring.Defs

variable (R : Type*) [CommMonoid R]

example (a b c d e f:R): a * (b * c) * (d * e * f) = a * f * (b * d) * (c * e) := by
  group

variable (R : Type*) [CommSemiring R]

example (a b c d e f:R): a * (b * c) * (d * e * f) = a * f * (b * d) * (c * e) := by
  group

I tried different tactics, like abel, ring, ring_nf, aesop, but no tactics solve it for commutative monoids.
Any suggestion, a part of writing the proof step by step?

[Kenny Lau]

I don't know what the correct tactic is, but a useful idiom is simp [mul_assoc, mul_left_comm, mul_comm]

[Aaron Liu]

import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Ring.Defs

section
variable (R : Type*) [CommMonoid R]

example (a b c d e f : R) : a * (b * c) * (d * e * f) = a * f * (b * d) * (c * e) := by
  ac_rfl
end

section
variable (R : Type*) [CommSemiring R]

example (a b c d e f : R) : a * (b * c) * (d * e * f) = a * f * (b * d) * (c * e) := by
  ac_rfl
end

[Weiyi Wang]

I remember there was a request to make abel handle (multiplicative) CommMonoid. It currently only works for additive ones

[Weiyi Wang]

Kenny Lau said:

I don't know what the correct tactic is, but a useful idiom is simp [mul_assoc, mul_left_comm, mul_comm]

I didn't know you could have mul_comm in simp. I thought it would send it to an infinite loop

[Kevin Buzzard]

Weiyi Wang said:

I remember there was a request to make abel handle (multiplicative) CommMonoid. It currently only works for additive ones

Yes, I was pushing to have the multiplicative tactic called mabel

[Yaël Dillies]

FWIW abel is likely going to become obsolete soon due to grind taking over its purpose