-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_piecewise_zero {m : MeasurableSpace α} (f : α →ₛ F) (μ : Measure α) {s : Set α}
    (hs : MeasurableSet s) : (piecewise s hs f 0).integral μ = f.integral (μ.restrict s)

Proof state:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ filter (fun x => x ≠ 0) (piecewise s hs f 0).range ⊆ filter (fun x => x ≠ 0) f.range

Tactic:
intro y hy

Result:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (piecewise s hs f 0).range
⊢ y ∈ filter (fun x => x ≠ 0) f.range

Proof state:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) f.range
⊢ (μ (⇑(piecewise s hs f 0) ⁻¹' {y})).toReal • y = ((μ.restrict s) (⇑f ⁻¹' {y})).toReal • y

Tactic:
dsimp

Result:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) f.range
⊢ (μ (s.piecewise (⇑f) 0 ⁻¹' {y})).toReal • y = ((μ.restrict s) (⇑f ⁻¹' {y})).toReal • y

Proof state:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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

Tactic:
rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩

Result:
case refine_1.intro.inl.intro
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
x : α
h₀ : f x ≠ 0
⊢ f x ∈ Set.range ⇑f ∧ f x ≠ 0

Proof state:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) (piecewise s hs f 0).range
⊢ y ∈ filter (fun x => x ≠ 0) f.range

Tactic:
simp only [mem_filter, mem_range, coe_piecewise, coe_zero, piecewise_eq_indicator,
  mem_range_indicator] at *

Result:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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

Proof state:
case refine_1.intro.inl.intro
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
x : α
h₀ : f x ≠ 0
⊢ f x ∈ Set.range ⇑f ∧ f x ≠ 0

Tactic:
exacts [(h₀ rfl).elim, ⟨Set.mem_range_self _, h₀⟩]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) f.range
⊢ (μ (s.piecewise (⇑f) 0 ⁻¹' {y})).toReal • y = ((μ.restrict s) (⇑f ⁻¹' {y})).toReal • y

Tactic:
rw [Set.piecewise_eq_indicator, indicator_preimage_of_not_mem,
  Measure.restrict_apply (f.measurableSet_preimage _)]

Result:
case refine_2.ht
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) f.range
⊢ 0 ∉ {y}

Proof state:
case refine_2.ht
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) f.range
⊢ 0 ∉ {y}

Tactic:
exact fun h₀ => (mem_filter.1 hy).2 (Eq.symm h₀)

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f

Tactic:
refine (integral_eq_sum_of_subset ?_).trans
    ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)

Result:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ filter (fun x => x ≠ 0) (piecewise s hs f 0).range ⊆ filter (fun x => x ≠ 0) f.range

case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ filter (fun x => x ≠ 0) f.range
⊢ (μ (⇑(piecewise s hs f 0) ⁻¹' {y})).toReal • y = ((μ.restrict s) (⇑f ⁻¹' {y})).toReal • y