-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem map_lintegral (g : β → ℝ≥0∞) (f : α →ₛ β) :
    (f.map g).lintegral μ = ∑ x ∈ f.range, g x * μ (f ⁻¹' {x})

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ ∑ x ∈ Finset.image g f.range, x * μ (⇑(map g f) ⁻¹' {x}) = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})

Tactic:
refine Finset.sum_image' _ fun b hb => ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
b : β
hb : b ∈ f.range
⊢ g b * μ (⇑(map g f) ⁻¹' {g b}) = ∑ j ∈ Finset.filter (fun j => g j = g b) f.range, g j * μ (⇑f ⁻¹' {j})

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ g (f a) * μ (⇑(map g f) ⁻¹' {g (f a)}) = ∑ j ∈ Finset.filter (fun j => g j = g (f a)) f.range, g j * μ (⇑f ⁻¹' {j})

Tactic:
rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∑ i ∈ Finset.filter (fun b => g b = g (f a)) f.range, g (f a) * μ (⇑f ⁻¹' {i}) =
    ∑ j ∈ Finset.filter (fun j => g j = g (f a)) f.range, g j * μ (⇑f ⁻¹' {j})

Proof state:
case intro.refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ Finset.filter (fun b => g b = g (f a)) f.range = Finset.filter (fun j => g j = g (f a)) f.range

Tactic:
congr

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∀ x ∈ Finset.filter (fun j => g j = g (f a)) f.range, g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Tactic:
intro x

Result:
case intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
x : β
⊢ x ∈ Finset.filter (fun j => g j = g (f a)) f.range → g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ (map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})

Tactic:
simp only [lintegral, range_map]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ ∑ x ∈ Finset.image g f.range, x * μ (⇑(map g f) ⁻¹' {x}) = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
b : β
hb : b ∈ f.range
⊢ g b * μ (⇑(map g f) ⁻¹' {g b}) = ∑ j ∈ Finset.filter (fun j => g j = g b) f.range, g j * μ (⇑f ⁻¹' {j})

Tactic:
rcases mem_range.1 hb with ⟨a, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ g (f a) * μ (⇑(map g f) ⁻¹' {g (f a)}) = ∑ j ∈ Finset.filter (fun j => g j = g (f a)) f.range, g j * μ (⇑f ⁻¹' {j})

Proof state:
case intro.refine_2.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
x : β
left✝ : x ∈ f.range
h : g x = g (f a)
⊢ g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Tactic:
rw [h]

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
x : β
⊢ x ∈ Finset.filter (fun j => g j = g (f a)) f.range → g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Tactic:
simp only [Finset.mem_filter]

Result:
case intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
x : β
⊢ x ∈ f.range ∧ g x = g (f a) → g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∑ i ∈ Finset.filter (fun b => g b = g (f a)) f.range, g (f a) * μ (⇑f ⁻¹' {i}) =
    ∑ j ∈ Finset.filter (fun j => g j = g (f a)) f.range, g j * μ (⇑f ⁻¹' {j})

Tactic:
refine Finset.sum_congr ?_ ?_

Result:
case intro.refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ Finset.filter (fun b => g b = g (f a)) f.range = Finset.filter (fun j => g j = g (f a)) f.range

case intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∀ x ∈ Finset.filter (fun j => g j = g (f a)) f.range, g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Proof state:
case intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
x : β
⊢ x ∈ f.range ∧ g x = g (f a) → g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Tactic:
rintro ⟨_, h⟩

Result:
case intro.refine_2.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
x : β
left✝ : x ∈ f.range
h : g x = g (f a)
⊢ g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})