no goals
M : Type ?u.482
N : Type ?u.485
S : Type u_1
M₀ : Type ?u.491
M₁ : Type ?u.494
R : Type ?u.497
G : Type ?u.500
G₀ : Type ?u.503
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p q : S
h : Commute p q
h₁ : IsIdempotentElem p
h₂ : IsIdempotentElem q
⊢ IsIdempotentElem (p * q)
rw [IsIdempotentElem, mul_assoc, ← mul_assoc q, ← h.eq, mul_assoc p, h₂.eq, ← mul_assoc, h₁.eq]