case intro.mk
α : Type u
M : Type u_1
N : Type ?u.56747
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1
α : Type u
M : Type u_1
N : Type ?u.56747
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, a * b = 1
rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩
no goals
case intro.mk
α : Type u
M : Type u_1
N : Type ?u.56747
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1
exact ⟨b, hab⟩