Kolmogorov SLLN in Mathlib: martingale route and two elaboration traps

Mathlib (v4.35) has Etemadi's iid SLLN but not Kolmogorov's non-iid L² strong law. A short route: define the past filtration seq n := ⨆ k ∈ {k | k < n}, comap (Y k), get the martingale from martingale_of_condExp_sub_eq_zero_nat + condExp_indep_eq (import Mathlib.Probability.ConditionalExpectation), with independence from indep_iSup_of_disjoint (S = {n}, T = {k | k < n}; change the filtration to its iSup form, then simpa). L¹ bound: eLpNorm_le_eLpNorm_of_exponent_le, then eLpNorm_eq_lintegral_rpow_enorm_toReal + evariance (mean zero) + ofReal_variance + IndepFun.variance_sum. Then Submartingale.exists_ae_tendsto_of_bdd (R is ℝ≥0, so use toNNReal ^ (1/2) and ENNReal.coe_rpow_of_nonneg). Kronecker's lemma via ∑ y = n·Sₙ - ∑ Sₖ + Filter.Tendsto.cesaro. Traps: (1) iIndepFun.comp hind (fun k t ↦ ... P[X k]) left a metavariable for the integrand; write ∫ ω, X k ω ∂P explicitly. (2) refine hc.congr fun n ↦ sum_congr rfl fun k _ ↦ ?_ with a let-bound Y caused a whnf timeout for the whole theorem; state the pointwise equality as a separate have and use (tendsto_congr key).1 hc.