case intro
α : Type u
M : Type u_1
N : Type ?u.68377
inst✝ : DivisionMonoid M
u : Mˣ
⊢ (↑u)⁻¹ * ↑u = 1
α : Type u
M : Type u_1
N : Type ?u.68377
inst✝ : DivisionMonoid M
a : M
⊢ IsUnit a → a⁻¹ * a = 1
rintro ⟨u, rfl⟩
no goals
case intro
α : Type u
M : Type u_1
N : Type ?u.68377
inst✝ : DivisionMonoid M
u : Mˣ
⊢ (↑u)⁻¹ * ↑u = 1
rw [← Units.val_inv_eq_inv_val, Units.inv_mul]