-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq_sum_of_subset [DecidablePred fun x : F => x ≠ 0] {f : α →ₛ F} {s : Finset F}
    (hs : {x ∈ f.range | x ≠ 0} ⊆ s) :
    f.integral μ = ∑ x ∈ s, (μ (f ⁻¹' {x})).toReal • x

Proof state:
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0

Tactic:
rcases hx.symm with (rfl | hx)

Result:
case inl
α : Type u_1
F : Type u_3
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) f.range ⊆ s
hx : 0 ∉ f.range ∨ 0 = 0
⊢ (μ (⇑f ⁻¹' {0})).toReal • 0 = 0

case inr
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ f.range
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0

Proof state:
α : Type u_1
F : Type u_3
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) f.range ⊆ s
⊢ integral μ f = ∑ x ∈ s, (μ (⇑f ⁻¹' {x})).toReal • x

Tactic:
rw [SimpleFunc.integral_eq_sum_filter, Finset.sum_subset hs]

Result:
α : Type u_1
F : Type u_3
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) f.range ⊆ s
⊢ ∀ x ∈ s, x ∉ filter (fun x => x ≠ 0) f.range → (μ (⇑f ⁻¹' {x})).toReal • x = 0

Proof state:
case inr
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0

Tactic:
rw [preimage_eq_empty] <;> simp [Set.disjoint_singleton_left, hx]

Result:
no goals

Proof state:
case inl
α : Type u_1
F : Type u_3
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) f.range ⊆ s
hx : 0 ∉ f.range ∨ 0 = 0
⊢ (μ (⇑f ⁻¹' {0})).toReal • 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
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) f.range ⊆ s
⊢ ∀ x ∈ s, x ∉ filter (fun x => x ≠ 0) f.range → (μ (⇑f ⁻¹' {x})).toReal • x = 0

Tactic:
rintro x - hx

Result:
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx : x ∉ filter (fun x => x ≠ 0) f.range
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0

Proof state:
case inr
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ f.range
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0

Tactic:
rw [SimpleFunc.mem_range] at hx

Result:
case inr
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0

Proof state:
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx : x ∉ filter (fun x => x ≠ 0) f.range
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0

Tactic:
rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx

Result:
α : Type u_1
F : Type u_3
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) f.range ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ (μ (⇑f ⁻¹' {x})).toReal • x = 0