case intro
R : Type u_1
inst✝ : Monoid R
b : R
a : Rˣ
⊢ IsRegular ↑a
R : Type u_1
inst✝ : Monoid R
a b : R
ua : IsUnit a
⊢ IsRegular a
rcases ua with ⟨a, rfl⟩
no goals
case intro
R : Type u_1
inst✝ : Monoid R
b : R
a : Rˣ
⊢ IsRegular ↑a
exact Units.isRegular a