α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x = 0
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
⊢ setToSimpleFunc T f = 0
simp_rw [setToSimpleFunc]
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
x : E
x✝ : x ∈ SimpleFunc.range f
⊢ ↑(T (↑f ⁻¹' {x})) x = 0
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x = 0
refine' sum_eq_zero fun x _ => _
case pos
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
x : E
x✝ : x ∈ SimpleFunc.range f
hx0 : x = 0
⊢ ↑(T (↑f ⁻¹' {x})) x = 0

case neg
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
x : E
x✝ : x ∈ SimpleFunc.range f
hx0 : ¬x = 0
⊢ ↑(T (↑f ⁻¹' {x})) x = 0
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
x : E
x✝ : x ∈ SimpleFunc.range f
⊢ ↑(T (↑f ⁻¹' {x})) x = 0
by_cases hx0 : x = 0
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
x : E
x✝ : x ∈ SimpleFunc.range f
hx0 : ¬x = 0
⊢ ↑(T (↑f ⁻¹' {x})) x = 0
rw [h_zero (f ⁻¹' ({x} : Set E)) (measurableSet_fiber _ _)
    (measure_preimage_lt_top_of_integrable f hf hx0),
  ContinuousLinearMap.zero_apply]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.131782
F' : Type u_3
G : Type ?u.131788
𝕜 : Type ?u.131791
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 α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T s = 0
f : α →ₛ E
hf : Integrable ↑f
x : E
x✝ : x ∈ SimpleFunc.range f
hx0 : x = 0
⊢ ↑(T (↑f ⁻¹' {x})) x = 0
simp [hx0]