Theorem: SciLean.Rand.push_E_affine (SciLean/Core/Rand/PushPullExpectation.lean)

State before:
R : Type ?u.27379
inst✝⁸ : RealScalar R
X : Type
inst✝⁷ : MeasurableSpace X
inst✝⁶ : AddCommGroup X
inst✝⁵ : Module ℝ X
Y : Type u_1
inst✝⁴ : AddCommGroup Y
inst✝³ : Module ℝ Y
inst✝² : MeasurableSpace Y
Z : Type u_2
inst✝¹ : AddCommGroup Z
inst✝ : Module ℝ Z
r : Rand X
φ : X → Y
f : Y → Z
hf : autoParam (IsAffineMap ℝ f) _auto✝
⊢ (r.𝔼 fun x => f (φ x)) = f (r.𝔼 φ)
Tactic:
rw[pull_E_affine (hf:=hf)]
State after:
no goals