Theorem: Probly.weightByDensity'_bind (Probly/PushPullE.lean)

State before:
X : Type
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : MeasurableSpace X
Y : Type ?u.1340
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.1457
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : MeasurableSpace Z
p q : ℝ
x : Rand (X × X)
⊢ (let x' ~ x
    Rand.pure (weightByDensity' p q x')) =
    weightByDensityM' p q x
Tactic:
rfl
State after:
no goals