case refine'_1
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ filter (fun x => x ≠ 0) (SimpleFunc.range (piecewise s hs f 0)) ⊆ filter (fun x => x ≠ 0) (SimpleFunc.range f)

case refine'_2
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ENNReal.toReal (↑↑μ (↑(piecewise s hs f 0) ⁻¹' {y})) • y = ENNReal.toReal (↑↑(Measure.restrict μ s) (↑f ⁻¹' {y})) • y
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ integral μ (piecewise s hs f 0) = integral (Measure.restrict μ s) f
refine' (integral_eq_sum_of_subset _).trans
    ((sum_congr rfl fun y hy => _).trans (integral_eq_sum_filter _ _).symm)
case refine'_1
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range (piecewise s hs f 0))
⊢ y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
case refine'_1
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ filter (fun x => x ≠ 0) (SimpleFunc.range (piecewise s hs f 0)) ⊆ filter (fun x => x ≠ 0) (SimpleFunc.range f)
intro y hy
case refine'_1
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : (y = 0 ∧ s ≠ Set.univ ∨ y ∈ ↑f '' s) ∧ y ≠ 0
⊢ y ∈ Set.range ↑f ∧ y ≠ 0
case refine'_1
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range (piecewise s hs f 0))
⊢ y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
simp only [mem_filter, mem_range, coe_piecewise, coe_zero, piecewise_eq_indicator,
  mem_range_indicator] at *
case refine'_1.intro.inl.intro
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
h₀ : 0 ≠ 0
⊢ 0 ∈ Set.range ↑f ∧ 0 ≠ 0

case refine'_1.intro.inr.intro.intro
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
x : α
h₀ : ↑f x ≠ 0
⊢ ↑f x ∈ Set.range ↑f ∧ ↑f x ≠ 0
case refine'_1
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : (y = 0 ∧ s ≠ Set.univ ∨ y ∈ ↑f '' s) ∧ y ≠ 0
⊢ y ∈ Set.range ↑f ∧ y ≠ 0
rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩
no goals
case refine'_1.intro.inl.intro
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
h₀ : 0 ≠ 0
⊢ 0 ∈ Set.range ↑f ∧ 0 ≠ 0

case refine'_1.intro.inr.intro.intro
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
x : α
h₀ : ↑f x ≠ 0
⊢ ↑f x ∈ Set.range ↑f ∧ ↑f x ≠ 0
exacts [(h₀ rfl).elim, ⟨Set.mem_range_self _, h₀⟩]
case refine'_2
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ENNReal.toReal (↑↑μ (Set.piecewise s (↑f) 0 ⁻¹' {y})) • y = ENNReal.toReal (↑↑(Measure.restrict μ s) (↑f ⁻¹' {y})) • y
case refine'_2
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ENNReal.toReal (↑↑μ (↑(piecewise s hs f 0) ⁻¹' {y})) • y = ENNReal.toReal (↑↑(Measure.restrict μ s) (↑f ⁻¹' {y})) • y
dsimp
case refine'_2.ht
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ¬0 ∈ {y}
case refine'_2
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ENNReal.toReal (↑↑μ (Set.piecewise s (↑f) 0 ⁻¹' {y})) • y = ENNReal.toReal (↑↑(Measure.restrict μ s) (↑f ⁻¹' {y})) • y
rw [Set.piecewise_eq_indicator, indicator_preimage_of_not_mem,
  Measure.restrict_apply (f.measurableSet_preimage _)]
no goals
case refine'_2.ht
α : Type u_1
E : Type ?u.125245
F : Type u_2
𝕜 : Type ?u.125251
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.125353
F' : Type ?u.125356
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ¬0 ∈ {y}
exact fun h₀ => (mem_filter.1 hy).2 (Eq.symm h₀)