Lean formalization of the Kolmogorov extension theorem