∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M],
  ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (Module.End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))))