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

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

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