Theorem: inv_mul_cancel_left (Evaluation/GroupsKnuthBendixSimp.lean)

State before:
G : Type
inv : G → G
mul : G → G → G
one : G
assocMul : ∀ (a b c : G), mul a (mul b c) = mul (mul a b) c
invLeft : ∀ (a : G), mul (inv a) a = one
mulOne : ∀ (a : G), mul a one = a
oneMul : ∀ (a : G), mul one a = a
invRight : ∀ (a : G), mul a (inv a) = one
x y : G
⊢ mul (inv x) (mul x y) = y
Tactic:
simp [assocMul, invLeft, mulOne, oneMul, invRight]
State after:
no goals