{R : Type u} →
  {n : Type w} →
    [inst : CommRing R] →
      [inst_1 : DecidableEq n] →
        [inst_2 : Fintype n] →
          (J : Matrix n n R) →
            {m : Type w} →
              [inst_3 : DecidableEq m] →
                [inst_4 : Fintype m] →
                  (e : Matrix n n R ≃ₐ[R] Matrix m m R) →
                    (∀ (A : Matrix n n R), (e A).transpose = e A.transpose) →
                      ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (e J))