Proving trivial identities under expectation

Stream: new members

[Duncan Skahan]

What tactic should I use for something like this?

import Mathlib

noncomputable section

open MeasureTheory ProbabilityTheory

variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
variable {X Y Z W : Ω → ℝ}

theorem trivial_identity : P[X*Y*Z*W] = P[Z*Y*X*W] := by
  sorry

[Derek Rhodes]

this works nicely:

theorem trivial_identity : P[X*Y*Z*W] = P[Z*Y*X*W] := by ring_nf