Theorem: Permutation.mul_left_cancel (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
x y z : Permutation n
h : x * y = x * z
this : (fun x_1 => inv x * x_1) (x * y) = (fun x_1 => inv x * x_1) (x * z)
⊢ y = z
Tactic:
conv at this =>
  dsimp; simp only [← mul_assoc, inv_mul, one_mul]
State after:
n : Nat
x y z : Permutation n
h : x * y = x * z
this : y = z
⊢ y = z

State before:
n : Nat
x y z : Permutation n
h : x * y = x * z
this : y = z
⊢ y = z
Tactic:
exact this
State after:
no goals