awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε₁ ≤
    (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) + ε₁

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
bc : (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) ≤ ε₂ - ε₁
⊢ (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) + ε₁ ≤ ε₂ - ε₁ + ε₁

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) ≤ ε₂ - ε₁

Tactic:
apply mul_div_le

Premises used: ENNReal.mul_div_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ ε₂ - ε₁ + ε₁ = ε₂

Tactic:
tsub_add_cancel_of_le hε₁₂.le

Premises used: tsub_add_cancel_of_le, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
rw :
  (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s)
rw₁ :
  (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁
rw₂ :
  (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁ ≤
    SimpleFunc.lintegral (const α (↑C : ℝ≥0∞)) (μ.restrict s) + ε₁
rw₃ :
  SimpleFunc.lintegral (const α (↑C : ℝ≥0∞)) (μ.restrict s) + ε₁ =
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε₁
rw₄ :
  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε₁ ≤
    (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) + ε₁
rw₅ : (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) + ε₁ ≤ ε₂ - ε₁ + ε₁
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂

Tactic:
calc
    (map (↑) ψ).lintegral (μ.restrict s) ≤
        (map (↑) φ).lintegral (μ.restrict s) + (map (↑) (ψ - φ)).lintegral (μ.restrict s) := by
      rw [← SimpleFunc.add_lintegral, ← SimpleFunc.map_add @ENNReal.coe_add]
      refine SimpleFunc.lintegral_mono (fun x => ?_) le_rfl
      simp only [add_tsub_eq_max, le_max_right, coe_map, Function.comp_apply, SimpleFunc.coe_add,
        SimpleFunc.coe_sub, Pi.add_apply, Pi.sub_apply, ENNReal.coe_max (φ x) (ψ x)]
    _ ≤ (map (↑) φ).lintegral (μ.restrict s) + ε₁ := by
      gcongr
      refine le_trans ?_ (hφ _ hψ).le
      exact SimpleFunc.lintegral_mono le_rfl Measure.restrict_le_self
    _ ≤ (SimpleFunc.const α (C : ℝ≥0∞)).lintegral (μ.restrict s) + ε₁ := by
      gcongr
      exact fun x ↦ ENNReal.coe_le_coe.2 (hC x)
    _ = C * μ s + ε₁ := by
      simp only [← SimpleFunc.lintegral_eq_lintegral, coe_const, lintegral_const,
        Measure.restrict_apply, MeasurableSet.univ, univ_inter, Function.const]
    _ ≤ C * ((ε₂ - ε₁) / C) + ε₁ := by gcongr
    _ ≤ ε₂ - ε₁ + ε₁ := by gcongr; apply mul_div_le
    _ = ε₂ := tsub_add_cancel_of_le hε₁₂.le

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.SimpleFunc.const, ENNReal.ofNNReal, HSub.hSub, MeasureTheory.Measure.restrict, tsub_add_cancel_of_le, HDiv.hDiv, LT.lt.le, DFunLike.coe, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
l : Filter ι
s : ι → Set α
hl : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
simp :
  ∀ (hl : ∀ (i : ℝ≥0∞) (i_1 : 0 < i), ∀ᶠ (a : ι) in l, ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) a < i) (i : ℝ≥0∞) (i_1 : 0 < i),
    ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < i
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α) in s i, f x ∂μ) l (𝓝 0)

Tactic:
simp only [ENNReal.nhds_zero, tendsto_iInf, tendsto_principal, mem_Iio,
    ← pos_iff_ne_zero] at hl ⊢

Premises used: ENNReal.nhds_zero, Set.mem_Iio, Filter.tendsto_principal, Filter.tendsto_iInf, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞) (i_1 : 0 < i), ∀ᶠ (a : ι) in l, ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
rcases :
  ∀ (δ : ℝ≥0∞) (δ0 : δ > 0) (hδ : ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε),
    ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε

Tactic:
rcases exists_pos_setLIntegral_lt_of_measure_lt h ε0.ne' with ⟨δ, δ0, hδ⟩

Premises used: MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞) (i_1 : 0 < i), ∀ᶠ (a : ι) in l, ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
δ : ℝ≥0∞
δ0 : δ > 0
hδ : ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε

Tactic:
(hl δ δ0).mono fun i => hδ _

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞) (i_1 : 0 < i), ∀ᶠ (a : ι) in l, ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
δ : ℝ≥0∞
δ0 : δ > 0
hδ : ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε

Tactic:
exact (hl δ δ0).mono fun i => hδ _

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂c • μ = c • ∫⁻ (a : α), f a ∂μ

Tactic:
simp only [lintegral, iSup_subtype', SimpleFunc.lintegral_smul, ENNReal.smul_iSup]

Premises used: iSup_subtype', ENNReal.smul_iSup, MeasureTheory.SimpleFunc.lintegral_smul, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
f : α → ℝ≥0∞
s : Set α
rw : ∫⁻ (a : α), f a ∂c • μ.restrict s = c • ∫⁻ (a : α) in s, f a ∂μ
rw₁ rw₂ : c • ∫⁻ (a : α) in s, f a ∂μ = c • ∫⁻ (a : α) in s, f a ∂μ
⊢ ∫⁻ (a : α) in s, f a ∂c • μ = c • ∫⁻ (a : α) in s, f a ∂μ

Tactic:
rw [Measure.restrict_smul, lintegral_smul_measure]

Premises used: MeasureTheory.Measure.restrict_smul, MeasureTheory.lintegral_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂0 = 0

Tactic:
simp [lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
simp :
  ⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      (↑x : α →ₛ ℝ≥0∞).lintegral μ + (↑x : α →ₛ ℝ≥0∞).lintegral ν =
    HAdd.hAdd (α := ℝ≥0∞)
      (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
        (↑x : α →ₛ ℝ≥0∞).lintegral μ)
      (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
        (↑x : α →ₛ ℝ≥0∞).lintegral ν)
⊢ ∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν

Tactic:
simp only [lintegral, SimpleFunc.lintegral_add, iSup_subtype']

Premises used: iSup_subtype', MeasureTheory.SimpleFunc.lintegral_add, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      (↑x : α →ₛ ℝ≥0∞).lintegral μ + (↑x : α →ₛ ℝ≥0∞).lintegral ν =
    HAdd.hAdd (α := ℝ≥0∞)
      (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
        (↑x : α →ₛ ℝ≥0∞).lintegral μ)
      (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
        (↑x : α →ₛ ℝ≥0∞).lintegral ν)

Tactic:
(ENNReal.iSup_add_iSup ?_).symm

Premises used: ENNReal.iSup_add_iSup, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
refine :
  ∀ (i j : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
    ∃ (k : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      (↑i : α →ₛ ℝ≥0∞).lintegral μ + (↑j : α →ₛ ℝ≥0∞).lintegral ν ≤
        (↑k : α →ₛ ℝ≥0∞).lintegral μ + (↑k : α →ₛ ℝ≥0∞).lintegral ν
⊢ ⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      (↑x : α →ₛ ℝ≥0∞).lintegral μ + (↑x : α →ₛ ℝ≥0∞).lintegral ν =
    HAdd.hAdd (α := ℝ≥0∞)
      (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
        (↑x : α →ₛ ℝ≥0∞).lintegral μ)
      (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
        (↑x : α →ₛ ℝ≥0∞).lintegral ν)

Tactic:
refine (ENNReal.iSup_add_iSup ?_).symm

Premises used: ENNReal.iSup_add_iSup, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0∞
hψ : LE.le (α := (a : α) → ℝ≥0∞) (⇑ψ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ ∃ (k : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
    (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ
                  hφ) :
              α →ₛ ℝ≥0∞).lintegral
          μ +
        (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) ψ
                  hψ) :
              α →ₛ ℝ≥0∞).lintegral
          ν ≤
      (↑k : α →ₛ ℝ≥0∞).lintegral μ + (↑k : α →ₛ ℝ≥0∞).lintegral ν

Tactic:
⟨⟨φ ⊔ ψ, sup_le hφ hψ⟩, ?_⟩

Premises used: Subtype.mk, Max.max, Exists.intro, sup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0∞
hψ : LE.le (α := (a : α) → ℝ≥0∞) (⇑ψ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
refine :
  (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ hφ) :
            α →ₛ ℝ≥0∞).lintegral
        μ +
      (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) ψ
                hψ) :
            α →ₛ ℝ≥0∞).lintegral
        ν ≤
    (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a)
                (φ ⊔ ψ) ⋯) :
            α →ₛ ℝ≥0∞).lintegral
        μ +
      (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a)
                (φ ⊔ ψ) ⋯) :
            α →ₛ ℝ≥0∞).lintegral
        ν
⊢ ∃ (k : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
    (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ
                  hφ) :
              α →ₛ ℝ≥0∞).lintegral
          μ +
        (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) ψ
                  hψ) :
              α →ₛ ℝ≥0∞).lintegral
          ν ≤
      (↑k : α →ₛ ℝ≥0∞).lintegral μ + (↑k : α →ₛ ℝ≥0∞).lintegral ν

Tactic:
refine ⟨⟨φ ⊔ ψ, sup_le hφ hψ⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0∞
hψ : LE.le (α := (a : α) → ℝ≥0∞) (⇑ψ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h₁ : φ ≤ φ ⊔ ψ
h₂ : ψ ≤ φ ⊔ ψ
⊢ (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ hφ) :
            α →ₛ ℝ≥0∞).lintegral
        μ +
      (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) ψ
                hψ) :
            α →ₛ ℝ≥0∞).lintegral
        ν ≤
    (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a)
                (φ ⊔ ψ) ⋯) :
            α →ₛ ℝ≥0∞).lintegral
        μ +
      (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a)
                (φ ⊔ ψ) ⋯) :
            α →ₛ ℝ≥0∞).lintegral
        ν

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0∞
hψ : LE.le (α := (a : α) → ℝ≥0∞) (⇑ψ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ φ ≤ φ ⊔ ψ

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0∞
hψ : LE.le (α := (a : α) → ℝ≥0∞) (⇑ψ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ ψ ≤ φ ⊔ ψ

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0∞
hψ : LE.le (α := (a : α) → ℝ≥0∞) (⇑ψ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ φ ≤ φ ⊔ ψ

Tactic:
exacts [le_sup_left, le_sup_right]

Premises used: le_sup_left, le_sup_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_4
s : Finset ι
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ ∫⁻ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i

Tactic:
let F : Measure α →+ ℝ≥0∞ :=
    { toFun := (lintegral · f),
      map_zero' := lintegral_zero_measure f,
      map_add' := lintegral_add_measure f }
  map_sum F μ s

Premises used: MeasureTheory.lintegral_add_measure, AddMonoidHom.mk, map_sum, ZeroHom.mk, MeasureTheory.lintegral_zero_measure, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_4
f : α → ℝ≥0∞
μ : ι → Measure α
simp_rw : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i
simp_rw₁ : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∫⁻ (a : α), f a ∂∑ i ∈ s, μ i
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (Measure.sum μ))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
simp_rw₃ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), ∑' (i : ι), g.lintegral (μ i))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
simp_rw₄ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
        ⨆ (s : Finset ι), ∑ i ∈ s, g.lintegral (μ i))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
simp_rw₅ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
        ⨆ (s : Finset ι), ∑ i ∈ s, g.lintegral (μ i))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), ∑ i ∈ s, g.lintegral (μ i))
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum, ← lintegral_finsetSum_measure,
    lintegral, SimpleFunc.lintegral_sum, ENNReal.tsum_eq_iSup_sum,
    SimpleFunc.lintegral_finsetSum, iSup_comm (ι := Finset ι)]

Premises used: MeasureTheory.SimpleFunc.lintegral_sum, MeasureTheory.SimpleFunc.lintegral_finsetSum, iSup_comm, ENNReal.tsum_eq_iSup_sum, MeasureTheory.lintegral_finsetSum_measure, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ HasSum (fun (i : ι) ↦ ∫⁻ (a : α), f a ∂μ i) (∫⁻ (a : α), f a ∂Measure.sum μ)

Tactic:
(lintegral_sum_measure f μ).symm ▸ ENNReal.summable.hasSum

Premises used: Eq.rec, ENNReal.summable, Summable.hasSum, Eq.symm, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
⊢ Subsingleton.{u_4 + 1} (Measure α)

Tactic:
have : Subsingleton (Measure α) := inferInstance
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
this : Subsingleton.{u_4 + 1} (Measure α)
⊢ ∫⁻ (a : α), f a ∂0 = 0

Tactic:
lintegral_zero_measure f

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
this : Subsingleton.{u_4 + 1} (Measure α)
⊢ ∫⁻ (x : α), f x ∂μ = 0

Tactic:
convert! lintegral_zero_measure f

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂0 = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = 0

Tactic:
rw [Measure.restrict_empty, lintegral_zero_measure]

Premises used: MeasureTheory.Measure.restrict_empty, MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
rw rw₁ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
⊢ ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α), f a ∂0 = 0

Tactic:
lintegral_zero_measure _

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : μ.restrict s = 0
⊢ ∫⁻ (x : α) in s, f x ∂μ = 0

Tactic:
convert! lintegral_zero_measure _

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.restrict s = 0

Tactic:
Measure.restrict_eq_zero.2 hs'

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.restrict s = 0

Tactic:
exact Measure.restrict_eq_zero.2 hs'

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h_1 : f =ᶠ[ae μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
dsimp : g (f a) = g (f' a)
⊢ Eq (α := ℝ≥0∞) ((fun (a : α) ↦ g (f a)) a) ((fun (a : α) ↦ g (f' a)) a)

Tactic:
dsimp only
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h_1 : f =ᶠ[ae μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
rw rw₁ : g (f' a) = g (f' a)
⊢ g (f a) = g (f' a)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁_1 : f₁ =ᶠ[ae μ] f₁'
h₂_1 : f₂ =ᶠ[ae μ] f₂'
g : β → γ → ℝ≥0∞
x : α
h₂ : f₂ x = f₂' x
h₁ : f₁ x = f₁' x
dsimp : g (f₁ x) (f₂ x) = g (f₁' x) (f₂' x)
⊢ Eq (α := ℝ≥0∞) ((fun (a : α) ↦ g (f₁ a) (f₂ a)) x) ((fun (a : α) ↦ g (f₁' a) (f₂' a)) x)

Tactic:
dsimp only
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁_1 : f₁ =ᶠ[ae μ] f₁'
h₂_1 : f₂ =ᶠ[ae μ] f₂'
g : β → γ → ℝ≥0∞
x : α
h₂ : f₂ x = f₂' x
h₁ : f₁ x = f₁' x
rw : g (f₁' x) (f₂ x) = g (f₁' x) (f₂' x)
rw₁ rw₂ : g (f₁' x) (f₂' x) = g (f₁' x) (f₂' x)
⊢ g (f₁ x) (f₂ x) = g (f₁' x) (f₂' x)

Tactic:
rw [h₁, h₂]