Theorem: SciLean.Rand.mean_add' (SciLean/Core/Rand/Rand.lean)

State before:
X : Type
Y : Type ?u.114836
Z : Type ?u.114839
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.114851
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.116048
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ x' + mean x = mean (x' + x)
Tactic:
simp[HAdd.hAdd,mean,𝔼,pure,bind]
State after:
X : Type
Y : Type ?u.114836
Z : Type ?u.114839
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.114851
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.116048
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ Add.add x' (∫' x, x ∂x.ℙ) =
    ∫' x,
      x ∂{ spec := erase fun φ => Erased.out x.spec fun x => φ (Add.add x' x),
          rand := StateT.bind x.rand fun x => StateT.pure (Add.add x' x) }.ℙ

State before:
X : Type
Y : Type ?u.114836
Z : Type ?u.114839
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.114851
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.116048
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ Add.add x' (∫' x, x ∂x.ℙ) =
    ∫' x,
      x ∂{ spec := erase fun φ => Erased.out x.spec fun x => φ (Add.add x' x),
          rand := StateT.bind x.rand fun x => StateT.pure (Add.add x' x) }.ℙ
Tactic:
sorry_proof
State after:
no goals