R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * (b * a) = y * (b * a)
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b
refine' fun x y xy => ab (_ : x * (b * a) = y * (b * a))
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * b * a = y * b * a
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * (b * a) = y * (b * a)
rw [← mul_assoc, ← mul_assoc]