awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ 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

Tactic:
⟨z, ?_, ?_⟩

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'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
refine_1 : aeSeq hf p b₁ ≤ aeSeq hf p z
refine_2 : 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:
refine ⟨z, ?_, ?_⟩
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p b₁ x ≤ aeSeq hf p z x
neg : ∀ (hx : x ∉ aeSeqSet hf p), aeSeq hf p b₁ x ≤ aeSeq hf p z x
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x

Tactic:
by_cases hx : x ∈ aeSeqSet hf p

Premises used: aeSeqSet
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
pos : f b₁ x ≤ aeSeq hf p z x
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Premises used: aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
pos : f b₁ x ≤ f z x
⊢ f b₁ x ≤ aeSeq hf p z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Premises used: aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
pos : f b₁ x ≤ f z x
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x

Tactic:
repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Premises used: aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- 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₂ 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₂]
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
neg : LE.le (α := ℝ≥0∞) (Nonempty.some ⋯) (Nonempty.some ⋯)
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x

Tactic:
simp only [aeSeq, hx, if_false]

Premises used: if_false, aeSeq
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ LE.le (α := ℝ≥0∞) (Nonempty.some ⋯) (Nonempty.some ⋯)

Tactic:
le_rfl

Premises used: le_rfl
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ LE.le (α := ℝ≥0∞) (Nonempty.some ⋯) (Nonempty.some ⋯)

Tactic:
exact le_rfl

Premises used: le_rfl
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p b₂ x ≤ aeSeq hf p z x
neg : ∀ (hx : x ∉ aeSeqSet hf p), aeSeq hf p b₂ x ≤ aeSeq hf p z x
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

Tactic:
by_cases hx : x ∈ aeSeqSet hf p

Premises used: aeSeqSet
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
pos : f b₂ x ≤ aeSeq hf p z x
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Premises used: aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
pos : f b₂ x ≤ f z x
⊢ f b₂ x ≤ aeSeq hf p z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Premises used: aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
pos : f b₂ x ≤ f z x
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

Tactic:
repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Premises used: aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- 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₂ 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₂]
-- 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₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
neg : LE.le (α := ℝ≥0∞) (Nonempty.some ⋯) (Nonempty.some ⋯)
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

Tactic:
simp only [aeSeq, hx, if_false]

Premises used: if_false, aeSeq
-- 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
⊢ Directed LE.le (aeSeq hf p)

Tactic:
have h_ae_seq_directed : Directed LE.le (aeSeq hf p) := by
    intro b₁ b₂
    obtain ⟨z, hz₁, hz₂⟩ := h_directed b₁ b₂
    refine ⟨z, ?_, ?_⟩ <;>
      · intro x
        by_cases hx : x ∈ aeSeqSet hf p
        · repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
          apply_rules [hz₁, hz₂]
        · simp only [aeSeq, hx, if_false]
          exact le_rfl
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), aeSeq hf p b a ∂μ

Tactic:
lintegral_iSup_directed_of_measurable (aeSeq.measurable hf p) h_ae_seq_directed

Premises used: aeSeq.measurable, MeasureTheory.lintegral_iSup_directed_of_measurable
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
h : ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p b a ∂μ
h₁ : Eq (α := ℝ≥0∞) (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ) (⨆ (b : β), ∫⁻ (a : α), aeSeq hf p b a ∂μ)
convert! : Measure α
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
convert! lintegral_iSup_directed_of_measurable (aeSeq.measurable hf p) h_ae_seq_directed using 1

Premises used: aeSeq.measurable, MeasureTheory.lintegral_iSup_directed_of_measurable
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
h : ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), (⨆ (i : β), aeSeq hf p i) a ∂μ
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p 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'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
h h₁ : ∫⁻ (a : α), (⨆ (n : β), aeSeq hf p n) a ∂μ = ∫⁻ (a : α), (⨆ (i : β), aeSeq hf p i) a ∂μ
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), (⨆ (i : β), aeSeq hf p i) a ∂μ

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

Premises used: MeasureTheory.lintegral_congr_ae, aeSeq.iSup, Filter.EventuallyEq.symm
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
h : Eq.{u_2 + 1} (α := β → ℝ≥0∞) (fun (b : β) ↦ ∫⁻ (a : α), f b a ∂μ) fun (b : β) ↦ ∫⁻ (a : α), aeSeq hf p b a ∂μ
⊢ Eq (α := ℝ≥0∞) (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ) (⨆ (b : β), ∫⁻ (a : α), aeSeq hf p b a ∂μ)

Tactic:
congr 1
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
h : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ = ∫⁻ (a : α), aeSeq hf p b a ∂μ
⊢ Eq.{u_2 + 1} (α := β → ℝ≥0∞) (fun (b : β) ↦ ∫⁻ (a : α), f b a ∂μ) fun (b : β) ↦ ∫⁻ (a : α), aeSeq hf p b a ∂μ

Tactic:
ext1 b
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
h : f b =ᶠ[ae μ] aeSeq hf p b
⊢ ∫⁻ (a : α), f b a ∂μ = ∫⁻ (a : α), aeSeq hf p b a ∂μ

Tactic:
rw [lintegral_congr_ae]

Premises used: MeasureTheory.lintegral_congr_ae
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
h : aeSeq hf p b =ᶠ[ae μ] f b
⊢ f b =ᶠ[ae μ] aeSeq hf p b

Tactic:
apply EventuallyEq.symm

Premises used: Filter.EventuallyEq.symm
-- 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
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ aeSeq hf p b =ᶠ[ae μ] f b

Tactic:
aeSeq.aeSeq_n_eq_fun_n_ae hf hp _

Premises used: aeSeq.aeSeq_n_eq_fun_n_ae
-- 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
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 _

Premises used: aeSeq.aeSeq_n_eq_fun_n_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
⊢ ∫⁻ (a : α), liminf (fun (n : ℕ) ↦ f n a) atTop ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i a ∂μ

Tactic:
simp only [liminf_eq_iSup_iInf_of_nat]

Premises used: Filter.liminf_eq_iSup_iInf_of_nat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
pos : ∀ (hu : ¬u.NeBot), ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
neg : ∀ (hu : u.NeBot), ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
by_cases! hu : ¬ u.NeBot

Premises used: Filter.NeBot
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : ¬u.NeBot
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∃ (g : ℕ → ι),
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop
        (𝓝 (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧
      Tendsto g atTop u

Tactic:
exists_seq_tendsto_liminf

Premises used: exists_seq_tendsto_liminf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
neg :
  ∀ (g : ℕ → ι)
    (hg :
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop
          (𝓝 (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧
        Tendsto g atTop u),
    ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
obtain ⟨g, hg⟩ : ∃ g : ℕ → ι,
        Tendsto (fun n => ∫⁻ a, f (g n) a ∂μ) atTop (𝓝 (liminf (fun i => ∫⁻ a, f i a ∂μ) u)) ∧
        Tendsto g atTop u :=
      exists_seq_tendsto_liminf

Premises used: exists_seq_tendsto_liminf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
g : ℕ → ι
hg :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop
      (𝓝 (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧
    Tendsto g atTop u
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ ∫⁻ (a : α), liminf (fun (n : ℕ) ↦ f (g n) a) atTop ∂μ

Tactic:
lintegral_mono fun a => hg.2.liminf_le_liminf_comp

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
g : ℕ → ι
hg :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop
      (𝓝 (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧
    Tendsto g atTop u
⊢ ∫⁻ (a : α), liminf (fun (n : ℕ) ↦ f (g n) a) atTop ∂μ ≤ liminf (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop

Tactic:
lintegral_liminf_nat_le' (fun n => h_meas (g n))

Premises used: _private.0.MeasureTheory.lintegral_liminf_nat_le'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
g : ℕ → ι
hg :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop
      (𝓝 (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧
    Tendsto g atTop u
⊢ Eq (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop) (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)

Tactic:
hg.1.liminf_eq

Premises used: Filter.Tendsto.liminf_eq, And.left
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
g : ℕ → ι
hg :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop
      (𝓝 (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧
    Tendsto g atTop u
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
calc
    _ ≤ ∫⁻ a, liminf (fun n => f (g n) a) atTop ∂μ :=
      lintegral_mono fun a => hg.2.liminf_le_liminf_comp
    _ ≤ liminf (fun n => ∫⁻ a, f (g n) a ∂μ) atTop :=
      lintegral_liminf_nat_le' (fun n => h_meas (g n))
    _ = _ := hg.1.liminf_eq

Premises used: _private.0.MeasureTheory.lintegral_liminf_nat_le', Filter.liminf, Filter.Tendsto.liminf_le_liminf_comp, Filter.atTop, Filter.Tendsto.liminf_eq, And.right, MeasureTheory.lintegral_mono, And.left, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), Measurable (f i)
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
lintegral_liminf_le' fun n => (h_meas n).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_liminf_le'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
e_f :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ f a) fun (a : α) ↦
    ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
e_f : ∀ (a : α), f a = ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ f a) fun (a : α) ↦
    ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a

Tactic:
ext a
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
e_f e_f₁ : f a = f a
⊢ f a = ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a

Tactic:
rw [iSup_eapprox_apply hf]

Premises used: MeasureTheory.SimpleFunc.iSup_eapprox_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hf₁ : ∀ (n : ℕ), Measurable (α := α) (β := ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) ↦ (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ

Tactic:
apply lintegral_iSup

Premises used: MeasureTheory.lintegral_iSup