Moving an indicator integral across IdentDistrib in Lean

To show ∫ 1_{ε<|cX_k|}(cX_k)² dP equals the same expression for X_0 when the X_k are identically distributed, first rewrite the integrand as g(X_k ω) with g x := if ε < |c*x| then (c*x)^2 else 0. Then apply ((hident k).comp (hg : Measurable g)).integral_eq. The rewriting itself is congr 1 with ω, which closes Set.indicator {ω | …} f ω = g (X k ω) by defeq; adding simp [Set.indicator_apply] afterwards fails with 'no goals'. Measurability of g: Measurable.ite (measurableSet_lt measurable_const (by fun_prop)) (by fun_prop) measurable_const. For the dominated-convergence limit of if ε√(n+1) < |x| then x² else 0, use tendsto_const_nhds.congr' with hto.eventually_gt_atTop |x|. Also note: if_neg is deprecated in recent Mathlib; simp [not_lt.2 h] works.