awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
e_s :
  ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)).lintegral μ
e_s₁ e_s₂ :
  ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ
⊢ ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    r * SimpleFunc.lintegral (eapprox f n) μ

Tactic:
rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]

Premises used: MeasureTheory.SimpleFunc.const_mul_lintegral, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ Measurable (α := α) (β := ℝ≥0∞) (⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞)

Tactic:
SimpleFunc.measurable _

Premises used: MeasureTheory.SimpleFunc.measurable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ Measurable (α := α) (β := ℝ≥0∞) (⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞)

Tactic:
exact SimpleFunc.measurable _

Premises used: MeasureTheory.SimpleFunc.measurable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
h_mono :
  HMul.hMul (β := ℝ≥0∞) r (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) r (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a)
    ((fun (n : ℕ) ↦ ((⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) i a)
    ((fun (n : ℕ) ↦ ((⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) j a)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
h_mono :
  LE.le (α := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) r (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) r (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
⊢ LE.le (α := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
monotone_eapprox _ h _

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
⊢ LE.le (α := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
exact monotone_eapprox _ h _

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
rw : r * ⨆ (i : ℕ), SimpleFunc.lintegral (eapprox f i) μ = r * ∫⁻ (a : α), f a ∂μ
rw₁ rw₂ : r * ⨆ (i : ℕ), SimpleFunc.lintegral (eapprox f i) μ = r * ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ
⊢ ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
rw [← ENNReal.mul_iSup, lintegral_eq_iSup_eapprox_lintegral hf]

Premises used: MeasureTheory.lintegral_eq_iSup_eapprox_lintegral, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ

Tactic:
have A : ∫⁻ a, f a ∂μ = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ

Tactic:
have B : ∫⁻ a, r * f a ∂μ = ∫⁻ a, r * hf.mk f a ∂μ :=
    lintegral_congr_ae (EventuallyEq.fun_comp hf.ae_eq_mk _)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
rw₁ : ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
rw₂ rw₃ : r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
rw [A, B, lintegral_const_mul _ hf.measurable_mk]

Premises used: MeasureTheory.lintegral_const_mul, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
rw :
  ⨆ (i : α →ₛ ℝ≥0∞), r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), i.lintegral μ ≤
    ∫⁻ (a : α), r * f a ∂μ
⊢ r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
rw [lintegral, ENNReal.mul_iSup]

Premises used: MeasureTheory.lintegral, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ⨆ (i : α →ₛ ℝ≥0∞), r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), i.lintegral μ ≤
    ∫⁻ (a : α), r * f a ∂μ

Tactic:
iSup_le fun s => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
refine :
  ∀ (s : α →ₛ ℝ≥0∞),
    r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), s.lintegral μ ≤
      ∫⁻ (a : α), r * f a ∂μ
⊢ ⨆ (i : α →ₛ ℝ≥0∞), r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), i.lintegral μ ≤
    ∫⁻ (a : α), r * f a ∂μ

Tactic:
refine iSup_le fun s => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
rw :
  ∀ (i : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
    r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
⊢ r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), s.lintegral μ ≤
    ∫⁻ (a : α), r * f a ∂μ

Tactic:
rw [ENNReal.mul_iSup, iSup_le_iff]

Premises used: iSup_le_iff, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
rw :
  (const α r * s).lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ r * f a), g.lintegral μ
⊢ r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
rw [← SimpleFunc.const_mul_lintegral, lintegral]

Premises used: MeasureTheory.SimpleFunc.const_mul_lintegral, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ (const α r * s).lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ r * f a), g.lintegral μ

Tactic:
le_iSup_of_le (const α r * s) (le_iSup_of_le (fun x => ?_) le_rfl)

Premises used: MeasureTheory.SimpleFunc.const, le_rfl, HMul.hMul, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
refine :
  ∀ (x : α),
    LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((const α r * s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((fun (a : α) ↦ r * f a) x : ℝ≥0∞)
⊢ (const α r * s).lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ r * f a), g.lintegral μ

Tactic:
refine le_iSup_of_le (const α r * s) (le_iSup_of_le (fun x => ?_) le_rfl)

Premises used: MeasureTheory.SimpleFunc.const, HMul.hMul, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
x : α
dsimp : HMul.hMul (β := ℝ≥0∞) r ((s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ≤ r * f x
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((const α r * s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((fun (a : α) ↦ r * f a) x : ℝ≥0∞)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
x : α
grw grw₁ : r * (fun (a : α) ↦ f a) x ≤ r * (fun (a : α) ↦ f a) x
⊢ HMul.hMul (β := ℝ≥0∞) r ((s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ≤ r * f x

Tactic:
grw [hs x]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
pos : ∀ (h : r = 0), ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
neg : ∀ (h : ¬r = 0), ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
by_cases h : r = 0
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : r = 0
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
apply : ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
apply le_antisymm _ (lintegral_const_mul_le r f)

Premises used: MeasureTheory.lintegral_const_mul_le, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
⊢ r * r⁻¹ = 1

Tactic:
have rinv : r * r⁻¹ = 1 := ENNReal.mul_inv_cancel h hr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rw : r * r⁻¹ = 1
⊢ r⁻¹ * r = 1

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ r * r⁻¹ = 1

Tactic:
rinv
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ r * r⁻¹ = 1

Tactic:
exact rinv
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ r⁻¹ * r = 1

Tactic:
have rinv' : r⁻¹ * r = 1 := by
    rw [mul_comm]
    exact rinv
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
⊢ r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ

Tactic:
have := lintegral_const_mul_le (μ := μ) r⁻¹ fun x => r * f x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ
⊢ r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), 1 * f a ∂μ

Tactic:
simp only [(mul_assoc _ _ _).symm, rinv'] at this

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), 1 * f a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ

Tactic:
simpa [(mul_assoc _ _ _).symm, rinv] using mul_le_mul_right this r

Premises used: mul_assoc, mul_le_mul_right, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
simp_rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

Tactic:
simp_rw [mul_comm, lintegral_const_mul r hf]

Premises used: mul_comm, MeasureTheory.lintegral_const_mul
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
simp_rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

Tactic:
simp_rw [mul_comm, lintegral_const_mul'' r hf]

Premises used: MeasureTheory.lintegral_const_mul'', mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
simp_rw : r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ
⊢ (∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ

Tactic:
simp_rw [mul_comm, lintegral_const_mul_le r f]

Premises used: MeasureTheory.lintegral_const_mul_le, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
simp_rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

Tactic:
simp_rw [mul_comm, lintegral_const_mul' r f hr]

Premises used: MeasureTheory.lintegral_const_mul', mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_3
inst : MeasurableSpace β
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
simp [lintegral_const_mul'' _ hg, lintegral_mul_const'' _ hf]

Premises used: MeasureTheory.lintegral_mul_const'', MeasureTheory.lintegral_const_mul''
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

Tactic:
@Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf

Premises used: Measurable.ennreal_induction
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
refine_1 :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (s.indicator fun (x : α) ↦ c)
refine_2 :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
            (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
              (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)
refine_3 :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)) →
          (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) fun (x : α) ↦ ⨆ (n : ℕ), f n x
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

Tactic:
refine
    @Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf

Premises used: Measurable.ennreal_induction
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
refine_1 :
  HMul.hMul (β := ℝ≥0∞) c ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ

Tactic:
rw [lintegral_indicator hs, lintegral_indicator (hm s hs), setLIntegral_const,
      setLIntegral_const]

Premises used: MeasureTheory.lintegral_indicator, MeasureTheory.setLIntegral_const
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw rw₁ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [h_trim_s]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
refine_1 : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
suffices h_trim_s : μ.trim hm s = μ s by rw [h_trim_s]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
trim_measurableSet_eq hm hs

Premises used: MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact trim_measurableSet_eq hm hs

Premises used: MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf : Measurable f_1
f g : α → ℝ≥0∞
refine_2 :
  Disjoint (Function.support f) (Function.support g) →
    Measurable f →
      Measurable g →
        (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
          (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
            (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)
⊢ Disjoint (Function.support f) (Function.support g) →
    Measurable f →
      Measurable g →
        (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
          (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
            (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
refine_2 :
  Measurable g →
    (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
      (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
        (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)
⊢ Measurable g →
    (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
      (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
        (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm

Tactic:
have h_m := lintegral_add_left (μ := Measure.trim μ hm) hf g
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
have h_m0 := lintegral_add_left (μ := μ) (Measurable.mono hf hm le_rfl) g
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
refine_2 :
  ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ.trim hm)
    (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
    ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
refine_2₁ :
  ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ)
    (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
    ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
refine_2₂ refine_2₃ refine_2₄ refine_2₅ :
  ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a + g a ∂μ)
    (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
    ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Tactic:
rwa [hf_prop, hg_prop, ← h_m0] at h_m
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
refine_3 : ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ
⊢ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ.trim hm =
    ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ

Tactic:
rw [lintegral_iSup hf hf_mono]

Premises used: MeasureTheory.lintegral_iSup