Theorem: mult_left (src/Group.lean)

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

State before:
α : Type u_1
G : group α
a b c : α
h : b = c
⊢ a * b = a * c
Tactic:
rw [h]
State after:
no goals