One version of Oseledets' Multiplicative Ergodic Theorem states that if $\sigma$ is an ergodic measure-preserving transformation of a space $(\Omega,\mathbb P)$ and if $A\colon\Omega\to GL(d,\mathbb R)$ is such that $\log\|A(\omega)\|$ and $\log\|(A(\omega))^{-1}\|$ are integrable, then there exist $k\le d$, $\infty>\lambda_1>\ldots>\lambda_k>-\infty$, $d_1,\ldots,d_k$ such that $d_1+\ldots+d_k=d$ and measurable maps $V_i\colon\Omega\to \mathcal G(d,d_i)$ (the Grassmannian of $d_i$-dimensional subspaces of $\mathbb R^d$) such that:

1. $A(\omega)V_i(\omega)=V_i(\sigma(\omega))$ a.s. (equivariance);
2. $V_1(\omega)\oplus \ldots\oplus V_k(\omega)=\mathbb R^d$ a.s. (direct sum decomposition);
3. For almost every $\omega$ and all $v\in V_i(\omega)\setminus\{0\}$, $\frac 1n\log\|A(\sigma^{n-1}\omega) \cdots A(\omega)v\|\to \lambda_i$ and $\frac 1n\log \| A(\sigma^{-n}\omega)^{-1}\cdots A(\sigma^{-1}\omega)^{-1}v\|\to-\lambda_i$.

Karlsson and Margulis (in a 1999 paper in CMP) proved a generalization of this theorem, where instead of a matrix cocycle, one has a cocycle mapping into the semi-contractions of a Hadamard metric space $(X,d)$: $a\colon \Omega\to SC(X)$ (a semi-contraction being a map of Lipschitz constant at most 1). They prove that given such a cocycle, and a measurable map $b\colon \Omega\to X$, $\lim_{n\to\infty}\frac 1nd(a(\omega)\circ a(\sigma\omega)\circ a(\sigma^{n-1}\omega)(b(x)),b(x))$ exists a.s; and $a(\omega)\circ a(\sigma\omega)\circ a(\sigma^{n-1}\omega)(b(x))$ shadows a geodesic at a sub-linear distance.

They then explain how the Oseledets theorem is a corollary of their theorem. Unfortunately, that part of the paper is extremely brief and assumes an understanding of the symmetric space $GL(d,\mathbb R)/O(d)$ (they don't directly describe the metric, but combining some statements in the paper, it appears from the paper that $d(A,B)$ is the Euclidean norm of the logarithms of the singular values of $A^{-1}B$ - I don't know how to prove this is a metric on $GL(d,\mathbb R)/O(d)$ for example; still less how to prove that it satisfies the required non-positive curvature conditions).

I'm looking for either a reference carrying out this deduction slowly, explaining explaining the necessary background; or failing that a reference giving enough background to make it feasible to understand the Karlsson-Margulis deduction.