-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_tsum [Countable β] {f : β → α → ℝ≥0∞} (hf : ∀ i, AEMeasurable (f i) μ) :
    ∫⁻ a, ∑' i, f i a ∂μ = ∑' i, ∫⁻ a, f i a ∂μ

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) s) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t)) ∧
    (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) t) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t))

Tactic:
constructor

Result:
case h.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) s) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t))

case h.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) t) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t))

Proof state:
case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun s a => ∑ i ∈ s, f i a

Tactic:
intro s t

Result:
case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) s) ((fun s a => ∑ i ∈ s, f i a) z) ∧
      (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) t) ((fun s a => ∑ i ∈ s, f i a) z)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ⨆ b, ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

Tactic:
simp [lintegral_finset_sum' _ fun i _ => hf i]

Result:
no goals

Proof state:
case h.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) t) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t))

Tactic:
exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_right

Result:
no goals

Proof state:
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a => ∑ i ∈ b, f i a) μ

Tactic:
intro b

Result:
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
b : Finset β
⊢ AEMeasurable (fun a => ∑ i ∈ b, f i a) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), ⨆ s, ∑ i ∈ s, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

Tactic:
rw [lintegral_iSup_directed]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ⨆ b, ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a => ∑ i ∈ b, f i a) μ

case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun s a => ∑ i ∈ s, f i a

Proof state:
case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) s) ((fun s a => ∑ i ∈ s, f i a) z) ∧
      (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) t) ((fun s a => ∑ i ∈ s, f i a) z)

Tactic:
use s ∪ t

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) s) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t)) ∧
    (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) t) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t))

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ

Tactic:
simp only [ENNReal.tsum_eq_iSup_sum]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), ⨆ s, ∑ i ∈ s, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

Proof state:
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
b : Finset β
⊢ AEMeasurable (fun a => ∑ i ∈ b, f i a) μ

Tactic:
exact Finset.aemeasurable_sum _ fun i _ => hf i

Result:
no goals

Proof state:
case h.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 => x1 ≤ x2) ((fun s a => ∑ i ∈ s, f i a) s) ((fun s a => ∑ i ∈ s, f i a) (s ∪ t))

Tactic:
exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_left

Result:
no goals