simp [assocMul, invLeft, mulOne, oneMul, invRight]
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
no goals