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

State before:
X Y : Type
Z : Type u_1
inst✝⁹ : MeasurableSpace X
inst✝⁸ : MeasurableSpace Y
R : Type ?u.86975
inst✝⁷ : RealScalar R
inst✝⁶ : AddCommGroup Y
inst✝⁵ : Module ℝ Y
inst✝⁴ : AddCommGroup Z
inst✝³ : Module ℝ Z
U : Type ?u.88172
inst✝² : AddCommGroup U
inst✝¹ : Module ℝ U
inst✝ : Nonempty X
f : X → Y
hf : Function.Injective f
r : Rand X
φ : X → Z
⊢ r.𝔼 φ =
    let invf := Function.invFun f;
    (r.map f).𝔼 fun y => φ (invf y)
Tactic:
simp [𝔼,Function.invFun_comp' hf]
State after:
no goals