α : Type u_1
E : Type ?u.222342
F : Type u_2
F' : Type u_3
G : Type ?u.222351
𝕜 : Type ?u.222354
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x}) + T' (↑f ⁻¹' {x})) x =
    ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x + ∑ x in SimpleFunc.range f, ↑(T' (↑f ⁻¹' {x})) x
α : Type u_1
E : Type ?u.222342
F : Type u_2
F' : Type u_3
G : Type ?u.222351
𝕜 : Type ?u.222354
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f
simp_rw [setToSimpleFunc, Pi.add_apply]
α : Type u_1
E : Type ?u.222342
F : Type u_2
F' : Type u_3
G : Type ?u.222351
𝕜 : Type ?u.222354
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, (↑(T (↑f ⁻¹' {x})) + ↑(T' (↑f ⁻¹' {x}))) x =
    ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x + ∑ x in SimpleFunc.range f, ↑(T' (↑f ⁻¹' {x})) x
α : Type u_1
E : Type ?u.222342
F : Type u_2
F' : Type u_3
G : Type ?u.222351
𝕜 : Type ?u.222354
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x}) + T' (↑f ⁻¹' {x})) x =
    ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x + ∑ x in SimpleFunc.range f, ↑(T' (↑f ⁻¹' {x})) x
push_cast
no goals
α : Type u_1
E : Type ?u.222342
F : Type u_2
F' : Type u_3
G : Type ?u.222351
𝕜 : Type ?u.222354
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, (↑(T (↑f ⁻¹' {x})) + ↑(T' (↑f ⁻¹' {x}))) x =
    ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x + ∑ x in SimpleFunc.range f, ↑(T' (↑f ⁻¹' {x})) x
simp_rw [Pi.add_apply, sum_add_distrib]