case intro
F : Type ?u.55988
G : Type ?u.55991
α : Type u_1
M : Type ?u.55997
N : Type ?u.56000
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹
F : Type ?u.55988
G : Type ?u.55991
α : Type u_1
M : Type ?u.55997
N : Type ?u.56000
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ IsUnit a⁻¹
rcases h with ⟨u, hu⟩
case intro
F : Type ?u.55988
G : Type ?u.55991
α : Type u_1
M : Type ?u.55997
N : Type ?u.56000
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹
case intro
F : Type ?u.55988
G : Type ?u.55991
α : Type u_1
M : Type ?u.55997
N : Type ?u.56000
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹
rw [←hu, ← Units.val_inv_eq_inv_val]
no goals
case intro
F : Type ?u.55988
G : Type ?u.55991
α : Type u_1
M : Type ?u.55997
N : Type ?u.56000
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹
exact Units.isUnit _