Theorem: mul_right_inv (src/Group.lean)

State before:
α : Type u_1
g : group α
⊢ ∀ (a : α), a * group.inv a = has_one.one
Tactic:
intro a
State after:
α : Type u_1
g : group α
a : α
⊢ a * group.inv a = has_one.one

State before:
α : Type u_1
g : group α
a : α
⊢ a * group.inv a = has_one.one
Tactic:
have h := g.mul_left_inv (group.inv a)
State after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one
Tactic:
rw [inv_invo] at h
State after:
α : Type u_1
g : group α
a : α
h : a * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one

State before:
α : Type u_1
g : group α
a : α
h : a * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one
Tactic:
exact h
State after:
no goals