α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.666025
G : Type ?u.666028
𝕜 : Type ?u.666031
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : { x // x ∈ simpleFunc E 1 μ }
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
    SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.666025
G : Type ?u.666028
𝕜 : Type ?u.666031
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : { x // x ∈ simpleFunc E 1 μ }
⊢ setToL1S T (f + g) = setToL1S T f + setToL1S T g
simp_rw [setToL1S]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.666025
G : Type ?u.666028
𝕜 : Type ?u.666031
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : { x // x ∈ simpleFunc E 1 μ }
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f + toSimpleFunc g)
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.666025
G : Type ?u.666028
𝕜 : Type ?u.666031
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : { x // x ∈ simpleFunc E 1 μ }
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
    SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)
rw [← SimpleFunc.setToSimpleFunc_add T h_add (SimpleFunc.integrable f)
    (SimpleFunc.integrable g)]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.666025
G : Type ?u.666028
𝕜 : Type ?u.666031
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : { x // x ∈ simpleFunc E 1 μ }
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f + toSimpleFunc g)
exact
  SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _)
    (add_toSimpleFunc f g)