-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iSup_directed [Countable β] {f : β → α → ℝ≥0∞} (hf : ∀ b, AEMeasurable (f b) μ)
    (h_directed : Directed (· ≤ ·) f) : ∫⁻ a, ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ a, f b a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
simp_rw [← iSup_apply]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
⊢ ∀ᵐ (x : α) ∂μ, p x fun i => f i x

Tactic:
filter_upwards [] with x i j

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j : β
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ aeSeq hf p z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ f z x

Proof state:
case h.e'_3.e_s.h.H
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ aeSeq hf p b =ᶠ[ae μ] f b

Tactic:
exact aeSeq.aeSeq_n_eq_fun_n_ae hf hp _

Result:
no goals

Proof state:
case h.e'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ∫⁻ (a : α), (⨆ i, aeSeq hf p i) a ∂?m.363903

Tactic:
rw [lintegral_congr_ae (aeSeq.iSup hf hp).symm]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ f z x

Tactic:
apply_rules [hz₁, hz₂]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j : β
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h_directed i j

Result:
case h.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j z : β
hz₁ : f i ≤ f z
hz₂ : f j ≤ f z
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

Tactic:
simp only [aeSeq, hx, if_false]

Result:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ ⋯.some ≤ ⋯.some

Proof state:
case h.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j z : β
hz₁ : f i ≤ f z
hz₂ : f j ≤ f z
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z

Tactic:
exact ⟨z, hz₁ x, hz₂ x⟩

Result:
no goals

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

Tactic:
let p : α → (β → ENNReal) → Prop := fun x f' => Directed LE.le f'

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ Directed LE.le (aeSeq hf p)

Tactic:
intro b₁ b₂

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ : β
⊢ ∃ z, aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z