Theorem: l1_1_5_i (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 * y = x * z → y = z
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 * y = x * z
⊢ y = z

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 * y = x * z
⊢ y = z
Tactic:
rwa [← mul_left_cancel_iff]
State after:
no goals