awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
⊢ ∫⁻ (x : α) in A ∩ {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x : α | g x < f x}, f x ∂μ ≤
    (ν : (a : Set α) → ℝ≥0∞) A

Tactic:
(add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq ?_

Premises used: LE.le.trans_eq, add_le_add, setOf, And.right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
refine :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | g a < f a}) : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) A
⊢ ∫⁻ (x : α) in A ∩ {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x : α | g x < f x}, f x ∂μ ≤
    (ν : (a : Set α) → ℝ≥0∞) A

Tactic:
refine (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq ?_

Premises used: LE.le.trans_eq, add_le_add, And.right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
simp :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (A \ {a : α | f a ≤ g a}) : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) A
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | g a < f a}) : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) A

Tactic:
simp only [← not_le, ← compl_setOf, ← diff_eq]

Premises used: not_le, Set.diff_eq, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (A \ {a : α | f a ≤ g a}) : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) A

Tactic:
measure_inter_add_diff _ (measurableSet_le hf.1 hg.1)

Premises used: measurableSet_le, setOf, MeasureTheory.measure_inter_add_diff, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (A \ {a : α | f a ≤ g a}) : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) A

Tactic:
exact measure_inter_add_diff _ (measurableSet_le hf.1 hg.1)

Premises used: measurableSet_le, MeasureTheory.measure_inter_add_diff, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
set :
  let c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a;
  ∀ (hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a), c = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
set c := ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a with hc
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
set :
  let d := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a);
  ∀ (hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)), c = d
⊢ c = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
set d := f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a with hd

Premises used: Nat.succ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
rw :
  ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∧
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
⊢ c = d

Tactic:
rw [le_antisymm_iff, hc, hd]

Premises used: le_antisymm_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
left : ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
right : max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∧
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
iSup₂_le fun n hn ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
left : ∀ (n : ℕ) (hn : n ≤ m + 1), f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
refine iSup₂_le fun n hn ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
left : ∀ (h : n ≤ m), f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
left₁ : ∀ (h : n = m.succ), f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
rcases Nat.of_le_succ hn with (h | h)

Premises used: Nat.of_le_succ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
h : n ≤ m
⊢ f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
le_sup_of_le_right (le_iSup₂ (f := fun k (_ : k ≤ m) ↦ f k a) n h)

Premises used: le_iSup₂, le_sup_of_le_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
h : n ≤ m
⊢ f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
exact le_sup_of_le_right (le_iSup₂ (f := fun k (_ : k ≤ m) ↦ f k a) n h)

Premises used: le_iSup₂, le_sup_of_le_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
h : n = m.succ
⊢ f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
h ▸ le_sup_left

Premises used: le_sup_left, Eq.rec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
h : n = m.succ
⊢ f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

Tactic:
exact h ▸ le_sup_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a

Tactic:
sup_le ?_ (biSup_mono fun n hn ↦ hn.trans m.le_succ)

Premises used: biSup_mono, Nat.le_succ, sup_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
right : f m.succ a ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
⊢ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a

Tactic:
refine sup_le ?_ (biSup_mono fun n hn ↦ hn.trans m.le_succ)

Premises used: biSup_mono, sup_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ f m.succ a ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a

Tactic:
@le_iSup₂ ℝ≥0∞ ℕ (fun i ↦ i ≤ m + 1) _ _ (m + 1) le_rfl

Premises used: le_rfl, le_iSup₂, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ f m.succ a ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a

Tactic:
exact @le_iSup₂ ℝ≥0∞ ℕ (fun i ↦ i ≤ m + 1) _ _ (m + 1) le_rfl

Premises used: le_rfl, le_iSup₂, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
zero : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x
zero₁ :
  ∀ (A : Set α),
    MeasurableSet A →
      ∫⁻ (x : α) in A, (fun (x : α) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x : ℝ≥0∞)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x

Tactic:
simp [(hf 0).1]

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : 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 : ℝ≥0∞)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A

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

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

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 _ _ _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν

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

Premises used: Set.Mem, Measurable.iSup, Measurable.iSup_Prop, setOf, LE.le, And.left, HAdd.hAdd, And.intro, OfNat.ofNat, MeasureTheory.Measure.LebesgueDecomposition.measurableLE
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
succ :
  ∀ (A : Set α) (hA : MeasurableSet A),
    ∫⁻ (x : α) in A, (fun (x : α) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k x : ℝ≥0∞)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) 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 ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
A : Set α
hA : MeasurableSet A
succ : ∫⁻ (a : α) in A, max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
⊢ ∫⁻ (x : α) in A, (fun (x : α) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k x : ℝ≥0∞)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A

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

Premises used: And.right, Nat.succ, MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A

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

Premises used: And.right, Nat.succ, MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
zero : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν
succ :
  ∀ (m_1 : ℕ) (hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m_1), f k x) ∈ measurableLE μ ν),
    (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m_1 + 1), f k x) ∈ measurableLE μ ν
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν

Tactic:
induction n with
  | zero =>
    constructor
    · simp [(hf 0).1]
    · intro A hA; simp [(hf 0).2 A hA]
  | succ m hm =>
    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 _ _ _
    refine ⟨.iSup fun n ↦ Measurable.iSup_Prop _ (hf n).1, fun A hA ↦ ?_⟩
    rw [this]; exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν

Tactic:
iSup_mem_measurableLE f hf n

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
h : ∀ (x : α), Eq (α := ℝ≥0∞) ((⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k ∈ measurableLE μ ν

Tactic:
convert! iSup_mem_measurableLE f hf n

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
x : α
⊢ Eq (α := ℝ≥0∞) ((⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_2
f : ℕ → α → ℝ≥0∞
⊢ Monotone.{0, u_2} (β := (x : α) → ℝ≥0∞) fun (n : ℕ) (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

Tactic:
fun _ _ hnm _ ↦ biSup_mono fun _ ↦ ge_trans hnm

Premises used: biSup_mono, Monotone, ge_trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_2
f : ℕ → α → ℝ≥0∞
x : α
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

Tactic:
fun _ _ hnm ↦ iSup_monotone f hnm x

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, Monotone
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_2
f : ℕ → α → ℝ≥0∞
n k : ℕ
hk : k ≤ n
⊢ f k ≤ fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

Tactic:
fun x ↦ le_iSup₂ (f := fun k (_ : k ≤ n) ↦ f k x) k hk

Premises used: le_iSup₂
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ Eq (α := ℝ≥0∞) ((fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ ∃ (u : ℕ → ℝ≥0∞),
    Monotone u ∧
      Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ

Tactic:
have h := @exists_seq_tendsto_sSup _ _ _ _ _ (measurableLEEval ν μ)
      ⟨0, 0, zero_mem_measurableLE, by simp⟩ (OrderTop.bddAbove _)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h :
  ∃ (u : ℕ → ℝ≥0∞),
    Monotone u ∧
      Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ
choose :
  ∀ (g : ℕ → ℝ≥0∞),
    Monotone g →
      ∀ (hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))) (f : (n : ℕ) → α → ℝ≥0∞)
        (hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ)
        (hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n),
        ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2

Tactic:
choose g _ hg₂ f hf₁ hf₂ using h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
⊢ let ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k;
  ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k

Tactic:
set ξ := ⨆ (n) (k) (_ : k ≤ n), f k with hξ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
refine_4 :
  ∀
    (this :
      Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
        (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))),
    sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
refine_1 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n) ν
refine_2 :
  ∀ᵐ (x : α) ∂ν, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x
refine_3 :
  ∀ᵐ (x : α) ∂ν,
    Filter.Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x)
      Filter.atTop (nhds ((⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x))
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν

Tactic:
have := @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k)
          (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν

Tactic:
tendsto_nhds_unique ?_ this

Premises used: tendsto_nhds_unique