Theorem: cancel_right (src/Group.lean)

State before:
α : Type u_1
G : group α
a b c : α
⊢ b * a = c * a → b = c
Tactic:
intro h
State after:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
⊢ b = c

State before:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
⊢ b = c
Tactic:
have h' := mult_right G (G.inv a) (b * a) (c * a) h
State after:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b * a * group.inv a = c * a * group.inv a
⊢ b = c

State before:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b * a * group.inv a = c * a * group.inv a
⊢ b = c
Tactic:
rw [G.mul_assoc, G.mul_assoc, mul_right_inv, G.mul_one, G.mul_one] at h'
State after:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b = c
⊢ b = c

State before:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b = c
⊢ b = c
Tactic:
exact h'
State after:
no goals