R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular (?m.13569 h * a)
rw [h]
no goals
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1
exact isRegular_one.left