∀ (R : Type u_3) (ι : Type u_2) [inst : CommRing R] (L : ι → Type u_1) [inst_1 : (i : ι) → LieRing (L i)]
  [inst_2 : (i : ι) → LieAlgebra R (L i)] (j : ι) {x y : DirectSum ι fun i => L i},
  (DirectSum.component R ι L j) ⁅x, y⁆ = ⁅(DirectSum.component R ι L j) x, (DirectSum.component R ι L j) y⁆