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

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

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