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

State before:
X : Type
Y : Type ?u.105470
Z : Type ?u.105473
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.105485
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.106682
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ mean x + x' = mean (x + x')
Tactic:
simp[HAdd.hAdd,mean,𝔼,pure,bind]
State after:
X : Type
Y : Type ?u.105470
Z : Type ?u.105473
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.105485
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.106682
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.105470
Z : Type ?u.105473
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.105485
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.106682
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