∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (toLieModuleHom : M →ₗ⁅R,L⁆ N) (invFun : N → M)
  (left_inv : Function.LeftInverse invFun (↑toLieModuleHom).toFun)
  (right_inv : Function.RightInverse invFun (↑toLieModuleHom).toFun) (toLieModuleHom_1 : M →ₗ⁅R,L⁆ N) (invFun_1 : N → M)
  (left_inv_1 : Function.LeftInverse invFun_1 (↑toLieModuleHom_1).toFun)
  (right_inv_1 : Function.RightInverse invFun_1 (↑toLieModuleHom_1).toFun),
  ({ toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toLieModuleHom = toLieModuleHom_1 ∧ invFun = invFun_1)