I'm not familiar with the details of Lean's implementation, so this may not be completely accurate.
I would guess that in the type theoretic base of lean, $Π$ types over universes are parametric, in the sense that there is nothing like a 'type case' operation. What, precisely, it means to be parametric in dependent type theory with universes and such is somewhat less clear than in the setting parametricity originated in. For instance, in the latter when you write
$$Π(S : *). T[S]$$
$T[S]$ it itself always a 'small' type that cannot embed $*$. But this is no longer the case for something like Lean's type theory, and that means that certain expected characterizations of parametricity no longer hold for those 'large' types. An example of how this would be 'fixed' is Internal Parametricity for Cubical Type Theory, where the expected parametricity rules only hold for certain sorts of 'discrete' types, and the universes are not discrete.
But also, aside from the core type theory, you should consider that due to its adoption of classical mathematics, the large scale culture of Lean is incompatible with parametricity. This is because principles like excluded middle are refuted by parametricity and vice versa. For instance, using a certain sort of excluded middle, you can write the non-parametric function:
$$
\mathsf{NP}(S, x) =
\begin{cases}
\mathsf{not}(x) & \mathrm{if}\ S = \mathsf{Bool} \\
x & \mathrm{otherwise}
\end{cases}
$$
I'm uncertain if you can define this function in this way given the peculiarities of Lean's type of propositions, even if you postulate excluded middle for said propositions. But, given the axiom of choice, which I've heard is also freely used, I'm relatively sure you could prove that there exists a non-parametric function. And in that scenario, it is of course inconsistent to assume that all functions are parametric.
So, even if the core type theory of Lean could admit parametricity, to make use of it you'd have to be careful about what additional postulates are in play in the libraries you interact with, because they can also be inconsistent with parametricity.
