case intro
α : Type u
M : Type u_1
N : Type ?u.68821
inst✝ : DivisionMonoid M
u : Mˣ
⊢ ↑u * (↑u)⁻¹ = 1
α : Type u
M : Type u_1
N : Type ?u.68821
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.68821
inst✝ : DivisionMonoid M
u : Mˣ
⊢ ↑u * (↑u)⁻¹ = 1
rw [← Units.val_inv_eq_inv_val, Units.mul_inv]