Theorem: cancel_left (src/Group.lean)

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

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

State before:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : group.inv a * (a * b) = group.inv a * (a * c)
⊢ b = c
Tactic:
rw [←G.mul_assoc, ←G.mul_assoc, G.mul_left_inv, G.one_mul, G.one_mul] at h'
State after:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : b = c
⊢ b = c

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