α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
⊢ ∀ (x : F), x ∈ s → ¬x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
⊢ integral μ f = ∑ x in s, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
rw [SimpleFunc.integral_eq_sum_filter, Finset.sum_subset hs]
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx : ¬x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
⊢ ∀ (x : F), x ∈ s → ¬x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
rintro x - hx
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx : ¬x ∈ SimpleFunc.range f ∨ x = 0
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx : ¬x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
rw [Finset.mem_filter, not_and_or, Ne.def, Classical.not_not] at hx
case inl
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
hx : ¬0 ∈ SimpleFunc.range f ∨ 0 = 0
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {0})) • 0 = 0

case inr
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx✝ : ¬x ∈ SimpleFunc.range f ∨ x = 0
hx : ¬x ∈ SimpleFunc.range f
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx : ¬x ∈ SimpleFunc.range f ∨ x = 0
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
rcases hx.symm with (rfl | hx)
case inr
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx✝ : ¬x ∈ SimpleFunc.range f ∨ x = 0
hx : ¬x ∈ Set.range ↑f
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
case inr
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx✝ : ¬x ∈ SimpleFunc.range f ∨ x = 0
hx : ¬x ∈ SimpleFunc.range f
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
rw [SimpleFunc.mem_range] at hx
case inr
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx✝ : ¬x ∈ SimpleFunc.range f ∨ x = 0
hx : ∀ (x_1 : α), ¬↑f x_1 = x
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
case inr
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx✝ : ¬x ∈ SimpleFunc.range f ∨ x = 0
hx : ¬x ∈ Set.range ↑f
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
simp only [Set.mem_range, not_exists] at hx
no goals
case inr
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
x : F
hx✝ : ¬x ∈ SimpleFunc.range f ∨ x = 0
hx : ∀ (x_1 : α), ¬↑f x_1 = x
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = 0
rw [preimage_eq_empty] <;> simp [Set.disjoint_singleton_left, hx]
no goals
case inl
α : Type u_2
E : Type ?u.107493
F : Type u_1
𝕜 : Type ?u.107499
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.107601
F' : Type ?u.107604
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
f : α →ₛ F
s : Finset F
hs : filter (fun x => x ≠ 0) (SimpleFunc.range f) ⊆ s
hx : ¬0 ∈ SimpleFunc.range f ∨ 0 = 0
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {0})) • 0 = 0
simp