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

State before:
X : Type
Y : Type ?u.76652
Z : Type ?u.76655
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.76667
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type u_1
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ ψ : X → U
hφ : CIntegrable φ r.ℙ
hψ : CIntegrable ψ r.ℙ
⊢ (r.𝔼 fun x => φ x + ψ x) = r.𝔼 φ + r.𝔼 ψ
Tactic:
simp[𝔼]
State after:
X : Type
Y : Type ?u.76652
Z : Type ?u.76655
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.76667
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type u_1
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ ψ : X → U
hφ : CIntegrable φ r.ℙ
hψ : CIntegrable ψ r.ℙ
⊢ ∫' x, φ x + ψ x ∂r.ℙ = ∫' x, φ x ∂r.ℙ + ∫' x, ψ x ∂r.ℙ

State before:
X : Type
Y : Type ?u.76652
Z : Type ?u.76655
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.76667
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type u_1
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ ψ : X → U
hφ : CIntegrable φ r.ℙ
hψ : CIntegrable ψ r.ℙ
⊢ ∫' x, φ x + ψ x ∂r.ℙ = ∫' x, φ x ∂r.ℙ + ∫' x, ψ x ∂r.ℙ
Tactic:
rw[cintegral_add] <;> assumption
State after:
no goals