Theorem: mult_right (src/Group.lean)

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

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