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 : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r_1 : ℝ≥0
right ha_1 : (↑r_1 : ℝ≥0∞) < 1
ha : r_1 < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r_1 * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r_1 : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
n : ℕ
r : ℝ≥0∞
h : r ∈ (SimpleFunc.map c rs).range
a : α
⊢ Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) a →
    (Membership.mem (γ := Set α) {a : α | r ≤ f n a} a ↔
      Membership.mem (γ := Set α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} a)

Tactic:
simp +contextual
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
simp :
  LE.le (α := ℝ≥0∞)
    (⨆ (n : ℕ),
      ∫⁻ (a : α),
        ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞)
          a ∂μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (n : ℕ), ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}).lintegral μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
simp only [← SimpleFunc.lintegral_eq_lintegral]

Premises used: MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
h :
  ∀ (n : ℕ) (a : α),
    ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞) a ≤
      f n a
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (n : ℕ),
      ∫⁻ (a : α),
        ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞)
          a ∂μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
gcongr with n a
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a}
n : ℕ
a : α
h : indicator {a : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a} (c ∘ (⇑rs : (a : α) → ℝ≥0)) a ≤ f n a
⊢ ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞) a ≤ f n a

Tactic:
simp only [coe_map, restrict_apply _ (h_meas _), (· ∘ ·)]

Premises used: Function.comp, MeasureTheory.SimpleFunc.coe_map, MeasureTheory.SimpleFunc.restrict_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a}
n : ℕ
a : α
⊢ indicator {a : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a} (c ∘ (⇑rs : (a : α) → ℝ≥0)) a ≤ f n a

Tactic:
indicator_apply_le id

Premises used: id, Set.indicator_apply_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a}
n : ℕ
a : α
⊢ indicator {a : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a} (c ∘ (⇑rs : (a : α) → ℝ≥0)) a ≤ f n a

Tactic:
exact indicator_apply_le id

Premises used: Set.indicator_apply_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
simp_rw : ∫⁻ (a : α), (⨆ (i : ℕ), f i) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [← iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
⊢ ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x

Tactic:
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p n x ≤ aeSeq hf p m x
neg : ∀ (hx : x ∉ aeSeqSet hf p), aeSeq hf p n x ≤ aeSeq hf p m x
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Tactic:
by_cases hx : x ∈ aeSeqSet hf p

Premises used: aeSeqSet
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ 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:
aeSeq.prop_of_mem_aeSeqSet hf hx hnm

Premises used: aeSeq.prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ 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

Premises used: aeSeq.prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ 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]

Premises used: le_rfl, if_false, aeSeq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
⊢ Monotone (aeSeq hf p)

Tactic:
have h_ae_seq_mono : Monotone (aeSeq hf p) := by
    intro n m hnm x
    by_cases hx : x ∈ aeSeqSet hf p
    · exact aeSeq.prop_of_mem_aeSeqSet hf hx hnm
    · simp only [aeSeq, hx, if_false, le_rfl]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
rw : ∫⁻ (a : α), (⨆ (n : ℕ), aeSeq hf p n) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), (⨆ (i : ℕ), f i) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n 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
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
simp_rw : ∫⁻ (a : α), ⨆ (i : ℕ), aeSeq hf p i a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), (⨆ (n : ℕ), aeSeq hf p n) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
rw : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
⊢ ∫⁻ (a : α), ⨆ (i : ℕ), aeSeq hf p i a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

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

Premises used: aeSeq.measurable, MeasureTheory.lintegral_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
e_s : ∀ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ = ∫⁻ (a : α), f n a ∂μ
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
congr with n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ 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:
lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae hf hp n)

Premises used: aeSeq.aeSeq_n_eq_fun_n_ae, MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ 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)

Premises used: aeSeq.aeSeq_n_eq_fun_n_ae, MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ

Tactic:
have : Monotone fun n => ∫⁻ x, f n x ∂μ := fun i j hij =>
    lintegral_mono_ae (h_mono.mono fun x hx => hx hij)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
rw [key]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ))

Tactic:
tendsto_atTop_iSup this

Premises used: tendsto_atTop_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ))

Tactic:
exact tendsto_atTop_iSup this

Premises used: tendsto_atTop_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
suffices : ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
suffices key : ∫⁻ x, F x ∂μ = ⨆ n, ∫⁻ x, f n x ∂μ by
    rw [key]
    exact tendsto_atTop_iSup this
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
rw : ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ

Tactic:
rw [← lintegral_iSup' hf h_mono]

Premises used: MeasureTheory.lintegral_iSup'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
refine : F =ᶠ[ae μ] fun (a : α) ↦ ⨆ (n : ℕ), f n a
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
a : α
hx_mono : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n a
hx_tendsto : Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (F a))
⊢ F a = ⨆ (n : ℕ), f n a

Tactic:
tendsto_nhds_unique hx_tendsto (tendsto_atTop_iSup hx_mono)

Premises used: tendsto_atTop_iSup, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))) x} x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ F x = (fun (a : α) ↦ (⨆ (n : ℕ), f n a : ℝ≥0∞)) x) x} x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (hx_mono : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n a)
    (hx_tendsto : Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (F a))), F a = ⨆ (n : ℕ), f n a
⊢ F =ᶠ[ae μ] fun (a : α) ↦ ⨆ (n : ℕ), f n a

Tactic:
filter_upwards [h_mono, h_tendsto] with _ hx_mono hx_tendsto using
    tendsto_nhds_unique hx_tendsto (tendsto_atTop_iSup hx_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
let :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_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
⊢ ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a

Tactic:
have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a :=
    (measure_eq_zero_iff_ae_notMem.1 hs.2.2).mono fun a ha n => if_neg ha
-- 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 : α
ha : ∀ (n : ℕ), g n a = f n a
⊢ Eq (α := ℝ≥0∞) ((fun (a : α) ↦ (⨆ (n : ℕ), f n a : ℝ≥0∞)) a) ((fun (a : α) ↦ (⨆ (n : ℕ), g n a : ℝ≥0∞)) a)

Tactic:
simp only [ha]