α : Type u_1
E : Type u_2
F : Type ?u.208871
𝕜 : Type ?u.208874
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.208976
F' : Type ?u.208979
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
ν : Measure α
f : α →ₛ E
hf : Integrable ↑f
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
α : Type u_1
E : Type u_2
F : Type ?u.208871
𝕜 : Type ?u.208874
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.208976
F' : Type ?u.208979
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
ν : Measure α
f : α →ₛ E
hf : Integrable ↑f
⊢ integral (μ + ν) f = integral μ f + integral ν f
simp_rw [integral_def]
α : Type u_1
E : Type u_2
F : Type ?u.208871
𝕜 : Type ?u.208874
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.208976
F' : Type ?u.208979
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
ν : Measure α
f : α →ₛ E
hf : Integrable ↑f
s : Set α
x✝ : MeasurableSet s
hμνs : ↑↑(μ + ν) s < ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
α : Type u_1
E : Type u_2
F : Type ?u.208871
𝕜 : Type ?u.208874
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.208976
F' : Type ?u.208979
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
ν : Measure α
f : α →ₛ E
hf : Integrable ↑f
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
refine' setToSimpleFunc_add_left'
  (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => _) hf
α : Type u_1
E : Type u_2
F : Type ?u.208871
𝕜 : Type ?u.208874
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.208976
F' : Type ?u.208979
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
ν : Measure α
f : α →ₛ E
hf : Integrable ↑f
s : Set α
x✝ : MeasurableSet s
hμνs : ↑↑μ s ≠ ⊤ ∧ ↑↑ν s ≠ ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
α : Type u_1
E : Type u_2
F : Type ?u.208871
𝕜 : Type ?u.208874
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.208976
F' : Type ?u.208979
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
ν : Measure α
f : α →ₛ E
hf : Integrable ↑f
s : Set α
x✝ : MeasurableSet s
hμνs : ↑↑(μ + ν) s < ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
rw [lt_top_iff_ne_top, Measure.coe_add, Pi.add_apply, ENNReal.add_ne_top] at hμνs
no goals
α : Type u_1
E : Type u_2
F : Type ?u.208871
𝕜 : Type ?u.208874
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.208976
F' : Type ?u.208979
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
ν : Measure α
f : α →ₛ E
hf : Integrable ↑f
s : Set α
x✝ : MeasurableSet s
hμνs : ↑↑μ s ≠ ⊤ ∧ ↑↑ν s ≠ ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
rw [weightedSMul_add_measure _ _ hμνs.1 hμνs.2]