Theorem: l1_1_5_ii (AlgebraI/Groups.lean)

State before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
⊢ x * z = y * z → x = y
Tactic:
intro h
State after:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
h : x * z = y * z
⊢ x = y

State before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
h : x * z = y * z
⊢ x = y
Tactic:
rwa [← mul_right_cancel_iff]
State after:
no goals