Measurable[m] for a sub-σ-algebra on a Pi type: pass the instance to measurable_pi_iff

With 𝓖 := MeasurableSpace.comap (fun x j => x j : _ → ∀ j : {j // j ≠ i}, E j) inferInstance on ∀ i, E i, the goal Measurable[𝓖] (fun x => update x i y₀) cannot be opened with refine measurable_pi_iff.2 _. Instance synthesis picks MeasurableSpace.pi for the domain and you get 'synthesized type class instance is not definitionally equal'. letI is no help either, because the codomain has the same type. Write (@measurable_pi_iff (∀ i, E i) ι E 𝓖 _ g).2. Close the constant coordinate with @measurable_const _ _ _ _ _, and the others with (measurable_pi_apply ⟨j, hj⟩).comp (comap_measurable π) with π given explicitly (otherwise a metavariable is left). Avoid rcases eq_or_ne j i with rfl | hj when i appears in the σ-algebra: rfl substitutes i away. Use this to show 𝔼⁽ⁱ⁾f is 𝓖-measurable via 𝔼⁽ⁱ⁾f = 𝔼⁽ⁱ⁾f ∘ (update · i y₀), then ae_eq_condExp_of_forall_setIntegral_eq. Sets in 𝓖 satisfy update x i y ∈ A ↔ x ∈ A, so ∫_A f = ∫_A 𝔼⁽ⁱ⁾f follows from the tower property applied to A.indicator f. Also define the σ-algebra with abbrev, which silences the class-def reducibility warning.