∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (M : Type u_3) [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] {χ₁ χ₂ χ₃ : ↥H → R} (hχ : χ₁ + χ₂ = χ₃),
  LieAlgebra.rootSpaceWeightSpaceProductAux R L H M hχ =
    { toFun := fun x => { toFun := fun m => ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }