{R : Type u} →
  {L : Type v} →
    {L' : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing L'] →
              [inst_4 : LieAlgebra R L'] →
                (toFun : L → L') →
                  (∀ (x y : L), toFun (x + y) = toFun x + toFun y) →
                    (∀ (m : R) (x : L), toFun (m • x) = (RingHom.id R) m • toFun x) →
                      (∀ {x y : L}, toFun ⁅x, y⁆ = ⁅toFun x, toFun y⁆) →
                        (invFun : L' → L) →
                          autoParam (Function.LeftInverse invFun toFun) LieEquiv.left_inv._autoParam →
                            autoParam (Function.RightInverse invFun toFun) LieEquiv.right_inv._autoParam → L ≃ₗ⁅R⁆ L'