Theorem: SciLean.Rand.swap_bind (SciLean/Core/Rand/Rand.lean)

State before:
X Y Z : Type
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
f : X → Y → Z
x : Rand X
y : Rand Y
⊢ (do
      let x' ← x
      let y' ← y
      pure (f x' y')) =
    do
    let y' ← y
    let x' ← x
    pure (f x' y')
Tactic:
sorry_proof
State after:
no goals