Cayley's theorem

import Mathlib

theorem cayley_thm {G : Type*} [Group G] : ∃ f : G →* Equiv.Perm G, Function.Injective f :=
  ⟨{
    toFun x := {
      toFun y := x * y
      invFun y := x⁻¹ * y
      left_inv y := inv_mul_cancel_left x y
      right_inv y := mul_inv_cancel_left x y
    }
    map_one' := DFunLike.ext _ _ one_mul
    map_mul' x y := DFunLike.ext _ _ (mul_assoc x y)
  }, fun a b hab => calc
    a = a * 1 := (mul_one a).symm
    _ = b * 1 := congrArg (· 1) hab
    _ = b := mul_one b⟩