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

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

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