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

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

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