case empty
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s → AEMeasurable (f b)
hf : ∀ (b : β), b ∈ ∅ → AEMeasurable (f b)
⊢ (∫⁻ (a : α), ∑ b in ∅, f b a ∂μ) = ∑ b in ∅, ∫⁻ (a : α), f b a ∂μ

case insert
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s✝ : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s✝ → AEMeasurable (f b)
a : β
s : Finset β
has : ¬a ∈ s
ih : (∀ (b : β), b ∈ s → AEMeasurable (f b)) → (∫⁻ (a : α), ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ (b : β), b ∈ insert a s → AEMeasurable (f b)
⊢ (∫⁻ (a_1 : α), ∑ b in insert a s, f b a_1 ∂μ) = ∑ b in insert a s, ∫⁻ (a : α), f b a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), b ∈ s → AEMeasurable (f b)
⊢ (∫⁻ (a : α), ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ (a : α), f b a ∂μ
induction' s using Finset.induction_on with a s has ih
no goals
case empty
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s → AEMeasurable (f b)
hf : ∀ (b : β), b ∈ ∅ → AEMeasurable (f b)
⊢ (∫⁻ (a : α), ∑ b in ∅, f b a ∂μ) = ∑ b in ∅, ∫⁻ (a : α), f b a ∂μ
simp
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s✝ : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s✝ → AEMeasurable (f b)
a : β
s : Finset β
has : ¬a ∈ s
ih : (∀ (b : β), b ∈ s → AEMeasurable (f b)) → (∫⁻ (a : α), ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ (b : β), b ∈ insert a s → AEMeasurable (f b)
⊢ (∫⁻ (a_1 : α), f a a_1 + ∑ b in s, f b a_1 ∂μ) = (∫⁻ (a_1 : α), f a a_1 ∂μ) + ∑ b in s, ∫⁻ (a : α), f b a ∂μ
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s✝ : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s✝ → AEMeasurable (f b)
a : β
s : Finset β
has : ¬a ∈ s
ih : (∀ (b : β), b ∈ s → AEMeasurable (f b)) → (∫⁻ (a : α), ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ (b : β), b ∈ insert a s → AEMeasurable (f b)
⊢ (∫⁻ (a_1 : α), ∑ b in insert a s, f b a_1 ∂μ) = ∑ b in insert a s, ∫⁻ (a : α), f b a ∂μ
simp only [Finset.sum_insert has]
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s✝ : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s✝ → AEMeasurable (f b)
a : β
s : Finset β
has : ¬a ∈ s
ih : (∀ (b : β), b ∈ s → AEMeasurable (f b)) → (∫⁻ (a : α), ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ (a : α), f b a ∂μ
hf : AEMeasurable (f a) ∧ ∀ (x : β), x ∈ s → AEMeasurable (f x)
⊢ (∫⁻ (a_1 : α), f a a_1 + ∑ b in s, f b a_1 ∂μ) = (∫⁻ (a_1 : α), f a a_1 ∂μ) + ∑ b in s, ∫⁻ (a : α), f b a ∂μ
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s✝ : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s✝ → AEMeasurable (f b)
a : β
s : Finset β
has : ¬a ∈ s
ih : (∀ (b : β), b ∈ s → AEMeasurable (f b)) → (∫⁻ (a : α), ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ (b : β), b ∈ insert a s → AEMeasurable (f b)
⊢ (∫⁻ (a_1 : α), f a a_1 + ∑ b in s, f b a_1 ∂μ) = (∫⁻ (a_1 : α), f a a_1 ∂μ) + ∑ b in s, ∫⁻ (a : α), f b a ∂μ
rw [Finset.forall_mem_insert] at hf
no goals
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.929424
δ : Type ?u.929427
m : MeasurableSpace α
μ ν : Measure α
s✝ : Finset β
f : β → α → ℝ≥0∞
hf✝ : ∀ (b : β), b ∈ s✝ → AEMeasurable (f b)
a : β
s : Finset β
has : ¬a ∈ s
ih : (∀ (b : β), b ∈ s → AEMeasurable (f b)) → (∫⁻ (a : α), ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ (a : α), f b a ∂μ
hf : AEMeasurable (f a) ∧ ∀ (x : β), x ∈ s → AEMeasurable (f x)
⊢ (∫⁻ (a_1 : α), f a a_1 + ∑ b in s, f b a_1 ∂μ) = (∫⁻ (a_1 : α), f a a_1 ∂μ) + ∑ b in s, ∫⁻ (a : α), f b a ∂μ
rw [lintegral_add_left' hf.1, ih hf.2]