-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iSup' {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, AEMeasurable (f n) μ)
    (h_mono : ∀ᵐ x ∂μ, Monotone fun n => f n x) : ∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μ

Proof state:
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Tactic:
by_cases hx : x ∈ aeSeqSet hf p

Result:
case pos
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ n, aeSeq hf p n) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [iSup_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), ⨆ i, aeSeq hf p i a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
⊢ ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [← iSup_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Tactic:
simp only [aeSeq, hx, if_false, le_rfl]

Result:
no goals

Proof state:
case e_s.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
n : ℕ
⊢ ∫⁻ (a : α), aeSeq hf p n a ∂μ = ∫⁻ (a : α), f n a ∂μ

Tactic:
exact lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae hf hp n)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), ⨆ i, aeSeq hf p i a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
rw [lintegral_iSup (aeSeq.measurable hf p) h_ae_seq_mono]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ⨆ n, ∫⁻ (a : α), aeSeq hf p n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ Monotone (aeSeq hf p)

Tactic:
intro n m hnm x

Result:
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ⨆ n, ∫⁻ (a : α), aeSeq hf p n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
congr with n

Result:
case e_s.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
n : ℕ
⊢ ∫⁻ (a : α), aeSeq hf p n a ∂μ = ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
let p : α → (ℕ → ℝ≥0∞) → Prop := fun _ f' => Monotone f'

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_mono

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

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

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ n, aeSeq hf p n) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
case pos
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Tactic:
exact aeSeq.prop_of_mem_aeSeqSet hf hx hnm

Result:
no goals