-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_eq_of_subset (f : α →ₛ ℝ≥0∞) {s : Finset ℝ≥0∞}
    (hs : ∀ x, f x ≠ 0 → μ (f ⁻¹' {f x}) ≠ 0 → f x ∈ s) :
    f.lintegral μ = ∑ x ∈ s, x * μ (f ⁻¹' {x})

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ f.lintegral μ = ∑ x ∈ s, x * μ (⇑f ⁻¹' {x})

Tactic:
refine Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ ∈ s

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ (a₁ : ℝ≥0∞) (h₁₁ : a₁ ∈ f.range) (h₁₂ : a₁ * μ (⇑f ⁻¹' {a₁}) ≠ 0) (a₂ : ℝ≥0∞) (h₂₁ : a₂ ∈ f.range)
    (h₂₂ : a₂ * μ (⇑f ⁻¹' {a₂}) ≠ 0), (fun r x x => r) a₁ h₁₁ h₁₂ = (fun r x x => r) a₂ h₂₁ h₂₂ → a₁ = a₂

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ b ∈ s,
    b * μ (⇑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ = b

case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0),
    a * μ (⇑f ⁻¹' {a}) = (fun r x x => r) a h₁ h₂ * μ (⇑f ⁻¹' {(fun r x x => r) a h₁ h₂})

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ ∈ s

Tactic:
simpa only [forall_mem_range, mul_ne_zero_iff, and_imp]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ ∃ a, ∃ (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ = b

Tactic:
refine ⟨b, ?_, hb, rfl⟩

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ b ∈ f.range

Proof state:
case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0),
    a * μ (⇑f ⁻¹' {a}) = (fun r x x => r) a h₁ h₂ * μ (⇑f ⁻¹' {(fun r x x => r) a h₁ h₂})

Tactic:
intros

Result:
case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
a✝ : ℝ≥0∞
h₁✝ : a✝ ∈ f.range
h₂✝ : a✝ * μ (⇑f ⁻¹' {a✝}) ≠ 0
⊢ a✝ * μ (⇑f ⁻¹' {a✝}) = (fun r x x => r) a✝ h₁✝ h₂✝ * μ (⇑f ⁻¹' {(fun r x x => r) a✝ h₁✝ h₂✝})

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ b ∈ s,
    b * μ (⇑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ = b

Tactic:
intro b _ hb

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ ∃ a, ∃ (h₁ : a ∈ f.range) (h₂ : a * μ (⇑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ = b

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ b ∈ f.range

Tactic:
rw [mem_range, ← preimage_singleton_nonempty]

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ (⇑f ⁻¹' {b}).Nonempty

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
a₁✝ : ℝ≥0∞
h₁₁✝ : a₁✝ ∈ f.range
h₁₂✝ : a₁✝ * μ (⇑f ⁻¹' {a₁✝}) ≠ 0
a₂✝ : ℝ≥0∞
h₂₁✝ : a₂✝ ∈ f.range
h₂₂✝ : a₂✝ * μ (⇑f ⁻¹' {a₂✝}) ≠ 0
a✝ : (fun r x x => r) a₁✝ h₁₁✝ h₁₂✝ = (fun r x x => r) a₂✝ h₂₁✝ h₂₂✝
⊢ a₁✝ = a₂✝

Tactic:
assumption

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ (⇑f ⁻¹' {b}).Nonempty

Tactic:
exact nonempty_of_measure_ne_zero (mul_ne_zero_iff.1 hb).2

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ (a₁ : ℝ≥0∞) (h₁₁ : a₁ ∈ f.range) (h₁₂ : a₁ * μ (⇑f ⁻¹' {a₁}) ≠ 0) (a₂ : ℝ≥0∞) (h₂₁ : a₂ ∈ f.range)
    (h₂₂ : a₂ * μ (⇑f ⁻¹' {a₂}) ≠ 0), (fun r x x => r) a₁ h₁₁ h₁₂ = (fun r x x => r) a₂ h₂₁ h₂₂ → a₁ = a₂

Tactic:
intros

Result:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
a₁✝ : ℝ≥0∞
h₁₁✝ : a₁✝ ∈ f.range
h₁₂✝ : a₁✝ * μ (⇑f ⁻¹' {a₁✝}) ≠ 0
a₂✝ : ℝ≥0∞
h₂₁✝ : a₂✝ ∈ f.range
h₂₂✝ : a₂✝ * μ (⇑f ⁻¹' {a₂✝}) ≠ 0
a✝ : (fun r x x => r) a₁✝ h₁₁✝ h₁₂✝ = (fun r x x => r) a₂✝ h₂₁✝ h₂₂✝
⊢ a₁✝ = a₂✝

Proof state:
case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
a✝ : ℝ≥0∞
h₁✝ : a✝ ∈ f.range
h₂✝ : a✝ * μ (⇑f ⁻¹' {a✝}) ≠ 0
⊢ a✝ * μ (⇑f ⁻¹' {a✝}) = (fun r x x => r) a✝ h₁✝ h₂✝ * μ (⇑f ⁻¹' {(fun r x x => r) a✝ h₁✝ h₂✝})

Tactic:
rfl

Result:
no goals