α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ ∑ x in Finset.image g (SimpleFunc.range f), x * ↑↑μ (↑(map g f) ⁻¹' {x}) =
    ∑ x in SimpleFunc.range f, g x * ↑↑μ (↑f ⁻¹' {x})
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ lintegral (map g f) μ = ∑ x in SimpleFunc.range f, g x * ↑↑μ (↑f ⁻¹' {x})
simp only [lintegral, range_map]
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
b : β
hb : b ∈ SimpleFunc.range f
⊢ g b * ↑↑μ (↑(map g f) ⁻¹' {g b}) =
    ∑ x in Finset.filter (fun c' => g c' = g b) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ ∑ x in Finset.image g (SimpleFunc.range f), x * ↑↑μ (↑(map g f) ⁻¹' {x}) =
    ∑ x in SimpleFunc.range f, g x * ↑↑μ (↑f ⁻¹' {x})
refine' Finset.sum_image' _ fun b hb => _
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ g (↑f a) * ↑↑μ (↑(map g f) ⁻¹' {g (↑f a)}) =
    ∑ x in Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
b : β
hb : b ∈ SimpleFunc.range f
⊢ g b * ↑↑μ (↑(map g f) ⁻¹' {g b}) =
    ∑ x in Finset.filter (fun c' => g c' = g b) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
rcases mem_range.1 hb with ⟨a, rfl⟩
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ ∑ x in Finset.filter (fun b => g b = g (↑f a)) (SimpleFunc.range f), g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) =
    ∑ x in Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ g (↑f a) * ↑↑μ (↑(map g f) ⁻¹' {g (↑f a)}) =
    ∑ x in Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]
case intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ Finset.filter (fun b => g b = g (↑f a)) (SimpleFunc.range f) =
    Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f)

case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ ∀ (x : β),
    x ∈ Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f) →
      g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ ∑ x in Finset.filter (fun b => g b = g (↑f a)) (SimpleFunc.range f), g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) =
    ∑ x in Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
refine' Finset.sum_congr _ _
no goals
case intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ Finset.filter (fun b => g b = g (↑f a)) (SimpleFunc.range f) =
    Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f)
congr
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
⊢ x ∈ Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f) →
    g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ ∀ (x : β),
    x ∈ Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f) →
      g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
intro x
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
⊢ x ∈ SimpleFunc.range f ∧ g x = g (↑f a) → g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
⊢ x ∈ Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f) →
    g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
simp only [Finset.mem_filter]
case intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
left✝ : x ∈ SimpleFunc.range f
h : g x = g (↑f a)
⊢ g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
⊢ x ∈ SimpleFunc.range f ∧ g x = g (↑f a) → g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
rintro ⟨_, h⟩
no goals
case intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.855234
δ : Type ?u.855237
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
left✝ : x ∈ SimpleFunc.range f
h : g x = g (↑f a)
⊢ g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
rw [h]