case refine'_1
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ SimpleFunc.range f) (h₂ : a * ↑↑μ (↑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ ∈ s

case refine'_2
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a₁ a₂ : ℝ≥0∞) (h₁₁ : a₁ ∈ SimpleFunc.range f) (h₁₂ : a₁ * ↑↑μ (↑f ⁻¹' {a₁}) ≠ 0) (h₂₁ : a₂ ∈ SimpleFunc.range f)
    (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
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (b : ℝ≥0∞), b ∈ s → b * ↑↑μ (↑f ⁻¹' {b}) ≠ 0 → ∃ a h₁ h₂, b = (fun r x x => r) a h₁ h₂

case refine'_4
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ SimpleFunc.range f) (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₂})
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ lintegral f μ = ∑ x in s, x * ↑↑μ (↑f ⁻¹' {x})
refine' Finset.sum_bij_ne_zero (fun r _ _ => r) _ _ _ _
no goals
case refine'_1
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ SimpleFunc.range f) (h₂ : a * ↑↑μ (↑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ ∈ s
simpa only [forall_range_iff, mul_ne_zero_iff, and_imp]
case refine'_2
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
a₁✝ a₂✝ : ℝ≥0∞
h₁₁✝ : a₁✝ ∈ SimpleFunc.range f
h₁₂✝ : a₁✝ * ↑↑μ (↑f ⁻¹' {a₁✝}) ≠ 0
h₂₁✝ : a₂✝ ∈ SimpleFunc.range f
h₂₂✝ : a₂✝ * ↑↑μ (↑f ⁻¹' {a₂✝}) ≠ 0
a✝ : (fun r x x => r) a₁✝ h₁₁✝ h₁₂✝ = (fun r x x => r) a₂✝ h₂₁✝ h₂₂✝
⊢ a₁✝ = a₂✝
case refine'_2
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a₁ a₂ : ℝ≥0∞) (h₁₁ : a₁ ∈ SimpleFunc.range f) (h₁₂ : a₁ * ↑↑μ (↑f ⁻¹' {a₁}) ≠ 0) (h₂₁ : a₂ ∈ SimpleFunc.range f)
    (h₂₂ : a₂ * ↑↑μ (↑f ⁻¹' {a₂}) ≠ 0), (fun r x x => r) a₁ h₁₁ h₁₂ = (fun r x x => r) a₂ h₂₁ h₂₂ → a₁ = a₂
intros
no goals
case refine'_2
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
a₁✝ a₂✝ : ℝ≥0∞
h₁₁✝ : a₁✝ ∈ SimpleFunc.range f
h₁₂✝ : a₁✝ * ↑↑μ (↑f ⁻¹' {a₁✝}) ≠ 0
h₂₁✝ : a₂✝ ∈ SimpleFunc.range f
h₂₂✝ : a₂✝ * ↑↑μ (↑f ⁻¹' {a₂✝}) ≠ 0
a✝ : (fun r x x => r) a₁✝ h₁₁✝ h₁₂✝ = (fun r x x => r) a₂✝ h₂₁✝ h₂₂✝
⊢ a₁✝ = a₂✝
assumption
case refine'_3
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
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₁ h₂, b = (fun r x x => r) a h₁ h₂
case refine'_3
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (b : ℝ≥0∞), b ∈ s → b * ↑↑μ (↑f ⁻¹' {b}) ≠ 0 → ∃ a h₁ h₂, b = (fun r x x => r) a h₁ h₂
intro b _ hb
case refine'_3
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
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 ∈ SimpleFunc.range f
case refine'_3
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
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₁ h₂, b = (fun r x x => r) a h₁ h₂
refine' ⟨b, _, hb, rfl⟩
case refine'_3
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
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
⊢ Set.Nonempty (↑f ⁻¹' {b})
case refine'_3
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
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 ∈ SimpleFunc.range f
rw [mem_range, ← preimage_singleton_nonempty]
no goals
case refine'_3
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
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
⊢ Set.Nonempty (↑f ⁻¹' {b})
exact nonempty_of_measure_ne_zero (mul_ne_zero_iff.1 hb).2
case refine'_4
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
a✝ : ℝ≥0∞
h₁✝ : a✝ ∈ SimpleFunc.range f
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₂✝})
case refine'_4
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ SimpleFunc.range f) (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₂})
intros
no goals
case refine'_4
α : Type u_1
β : Type ?u.852623
γ : Type ?u.852626
δ : Type ?u.852629
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
a✝ : ℝ≥0∞
h₁✝ : a✝ ∈ SimpleFunc.range f
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₂✝})
rfl