-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem iSup_mem_measurableLE (f : ℕ → α → ℝ≥0∞) (hf : ∀ n, f n ∈ measurableLE μ ν) (n : ℕ) :
    (fun x ↦ ⨆ (k) (_ : k ≤ n), f k x) ∈ measurableLE μ ν

Proof state:
case zero.right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ ∀ (A : Set α), MeasurableSet A → ∫⁻ (x : α) in A, (fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x) x ∂μ ≤ ν A

Tactic:
intro A hA

Result:
case zero.right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x) x ∂μ ≤ ν A

Proof state:
case zero
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ (fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν

Tactic:
constructor

Result:
case zero.left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ Measurable fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x

case zero.right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ ∀ (A : Set α), MeasurableSet A → ∫⁻ (x : α) in A, (fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x) x ∂μ ≤ ν A

Proof state:
case zero.left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ Measurable fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x

Tactic:
simp [(hf 0).1]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ (fun x => ⨆ k, ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν

Tactic:
induction' n with m hm

Result:
case zero
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ (fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν

case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
⊢ (fun x => ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν

Proof state:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a => f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ∂μ ≤ ν A

Tactic:
exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA

Result:
no goals

Proof state:
case zero.right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun x => ⨆ k, ⨆ (_ : k ≤ 0), f k x) x ∂μ ≤ ν A

Tactic:
simp [(hf 0).2 A hA]

Result:
no goals

Proof state:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a => f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ (fun x => ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν

Tactic:
refine ⟨.iSup fun n ↦ Measurable.iSup_Prop _ (hf n).1, fun A hA ↦ ?_⟩

Result:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a => f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun x => ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) x ∂μ ≤ ν A

Proof state:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a => f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun x => ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) x ∂μ ≤ ν A

Tactic:
rw [this]

Result:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a => f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ∂μ ≤ ν A

Proof state:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
⊢ (fun x => ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν

Tactic:
have :
  (fun a : α ↦ ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a ↦
    f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
  funext fun _ ↦ iSup_succ_eq_sup _ _ _

Result:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a => f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ (fun x => ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν