Theorem: SciLean.Prob.Rand.add_E (SciLean/Modules/Prob/Rand.lean)

State before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.30017
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.30023
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
φ ψ : X → Y
⊢ (E x fun x => φ x + ψ x) = E x φ + E x ψ
Tactic:
simp only [E]
State after:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.30017
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.30023
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
φ ψ : X → Y
⊢ ∫ (x' : X), φ x' + ψ x' ∂↑x.μ = ∫ (x' : X), φ x' ∂↑x.μ + ∫ (x' : X), ψ x' ∂↑x.μ

State before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.30017
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.30023
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
φ ψ : X → Y
⊢ ∫ (x' : X), φ x' + ψ x' ∂↑x.μ = ∫ (x' : X), φ x' ∂↑x.μ + ∫ (x' : X), ψ x' ∂↑x.μ
Tactic:
sorry
State after:
no goals