awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), g n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), g n a ∂μ

Tactic:
(lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))

Premises used: Measurable.piecewise, And.right, And.left, MeasureTheory.lintegral_iSup, measurable_const, monotone_nat_of_le_succ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), g n a ∂μ) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]

Premises used: MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
f₁ : ∀ (n : ℕ) (a : α), g n a ≤ g (n + 1) a
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
calc
    ∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ :=
      lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
    _ = ⨆ n, ∫⁻ a, g n a ∂μ :=
      (lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))
    _ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]

Premises used: Measurable.piecewise, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, And.right, And.left, MeasureTheory.lintegral_iSup, measurable_const, monotone_nat_of_le_succ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
simp : (if a ∈ s then 0 else f n a) ≤ if a ∈ s then 0 else f (n + 1) a
⊢ g n a ≤ g (n + 1) a

Tactic:
simp only [g]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
pos : ∀ (h : a ∈ s), LE.le (α := ℝ≥0∞) 0 0
neg : ∀ (h : a ∉ s), f n a ≤ f (n + 1) a
⊢ (if a ∈ s then 0 else f n a) ≤ if a ∈ s then 0 else f (n + 1) a

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∈ s
⊢ LE.le (α := ℝ≥0∞) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
⊢ a ∉ {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a}

Tactic:
have := Set.notMem_subset hs.1 h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
this : a ∉ {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a}
⊢ ∀ (x : ℕ), f x a ≤ f x.succ a

Tactic:
simp only [not_forall, not_le, mem_setOf_eq, not_exists, not_lt] at this

Premises used: not_le, not_exists, Set.mem_setOf_eq, not_lt, Classical.not_forall
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
this : ∀ (x : ℕ), f x a ≤ f x.succ a
⊢ f n a ≤ f (n + 1) a

Tactic:
this n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
this : ∀ (x : ℕ), f x a ≤ f x.succ a
⊢ f n a ≤ f (n + 1) a

Tactic:
exact this n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
intro : ∀ (val : Encodable β), ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
cases nonempty_encodable β

Premises used: nonempty_encodable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
intro : IsEmpty β → ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
intro₁ : Nonempty β → ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : IsEmpty β
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
intro : ∀ (inhabited_h : Inhabited β), ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
a : α
⊢ Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
    (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)

Tactic:
le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)

Premises used: le_iSup, le_antisymm, Directed.sequence, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
a : α
refine : ∀ (b : β), f b a ≤ ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a
⊢ Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
    (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)

Tactic:
refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)

Premises used: le_iSup, le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
a : α
b : β
⊢ f b a ≤ ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a

Tactic:
le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)

Premises used: HAdd.hAdd, le_iSup_of_le, Directed.le_sequence, Encodable.encode, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
a : α
b : β
⊢ f b a ≤ ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a

Tactic:
exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)

Premises used: HAdd.hAdd, le_iSup_of_le, Encodable.encode, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
⊢ ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)

Tactic:
have : ∀ a, ⨆ b, f b a = ⨆ n, f (h_directed.sequence f n) a := by
    intro a
    refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)
    exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ =
    ∫⁻ (a : α), ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ

Tactic:
simp only [this]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ =
    ⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ

Tactic:
(lintegral_iSup (fun n => hf _) h_directed.sequence_mono)

Premises used: MeasureTheory.lintegral_iSup, Directed.sequence, Directed.sequence_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
⊢ Eq (α := ℝ≥0∞)
    (⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ)
    (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ)

Tactic:
le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
refine_1 :
  ∀ (n : ℕ),
    ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ ≤
      ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
refine_2 :
  ∀ (b : β),
    ∫⁻ (a : α), f b a ∂μ ≤
      ⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ
⊢ Eq (α := ℝ≥0∞)
    (⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ)
    (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ)

Tactic:
refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
n : ℕ
⊢ ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ ≤
    ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
le_iSup (fun b => ∫⁻ a, f b a ∂μ) _

Premises used: le_iSup, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
n : ℕ
⊢ ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ ≤
    ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _

Premises used: le_iSup, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
b : β
⊢ ∫⁻ (a : α), f b a ∂μ ≤
    ⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ

Tactic:
le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)

Premises used: MeasureTheory.lintegral_mono, HAdd.hAdd, le_iSup_of_le, Directed.le_sequence, Encodable.encode, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
b : β
⊢ ∫⁻ (a : α), f b a ∂μ ≤
    ⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ

Tactic:
exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)

Premises used: HAdd.hAdd, le_iSup_of_le, Encodable.encode, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
f₁ :
  ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ =
    ∫⁻ (a : α), ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ
f₂ :
  Eq (α := ℝ≥0∞)
    (⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ)
    (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ)
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
calc
    ∫⁻ a, ⨆ b, f b a ∂μ = ∫⁻ a, ⨆ n, f (h_directed.sequence f n) a ∂μ := by simp only [this]
    _ = ⨆ n, ∫⁻ a, f (h_directed.sequence f n) a ∂μ :=
      (lintegral_iSup (fun n => hf _) h_directed.sequence_mono)
    _ = ⨆ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
      · exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _
      · exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)

Premises used: MeasureTheory.lintegral_iSup, Directed.sequence_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
simp_rw : ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
simp_rw [← iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
h :
  ∀ (x : α) (i j : β),
    ∃ (z : β),
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
        LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)
⊢ ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x

Tactic:
filter_upwards [] with x i j
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
x : α
i j : β
h :
  ∀ (z : β) (hz₁ : f i ≤ f z) (hz₂ : f j ≤ f z),
    ∃ (z : β),
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
        LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)
⊢ ∃ (z : β),
    LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h_directed i j
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
x : α
i j z : β
hz₁ : f i ≤ f z
hz₂ : f j ≤ f z
⊢ ∃ (z : β),
    LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
x : α
i j z : β
hz₁ : f i ≤ f z
hz₂ : f j ≤ f z
⊢ ∃ (z : β),
    LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)

Tactic:
exact ⟨z, hz₁ x, hz₂ x⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
⊢ ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x

Tactic:
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := by
    filter_upwards [] with x i j
    obtain ⟨z, hz₁, hz₂⟩ := h_directed i j
    exact ⟨z, hz₁ x, hz₂ x⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ : β
obtain :
  ∀ (z : β) (hz₁ : f b₁ ≤ f z) (hz₂ : f b₂ ≤ f z),
    ∃ (z : β), aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
⊢ ∃ (z : β), aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z

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