awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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)
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂
have rw₁ : (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤
  (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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) + ε₁
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂
have rw₂ : (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁ ≤
  SimpleFunc.lintegral (const α (↑C : ℝ≥0∞)) (μ.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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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) + ε₁
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂
have rw₃ : SimpleFunc.lintegral (const α (↑C : ℝ≥0∞)) (μ.restrict s) + ε₁ =
  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε₁
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞) + ε₁
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂
have rw₄ : HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε₁ ≤
  (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) + ε₁
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞)) + ε₁
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂
have rw₅ : (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) + ε₁ ≤ ε₂ - ε₁ + ε₁
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α) in s i, f x ∂μ) l (𝓝 0)
have 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
Tactic: simp only [ENNReal.nhds_zero, tendsto_iInf, tendsto_principal, mem_Iio,
    ← pos_iff_ne_zero] at hl ⊢
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε
have 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 ∂μ < ε
Tactic: rcases exists_pos_setLIntegral_lt_of_measure_lt h ε0.ne' with ⟨δ, δ0, hδ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 α
⊢ ∫⁻ (a : α) in s, f a ∂c • μ = c • ∫⁻ (a : α) in s, f a ∂μ
have rw : ∫⁻ (a : α), f a ∂c • μ.restrict s = c • ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [Measure.restrict_smul, lintegral_smul_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∫⁻ (a : α) in s, f a ∂c • μ = c • ∫⁻ (a : α) in s, f a ∂μ
have rw₁ : c • ∫⁻ (a : α) in s, f a ∂μ = c • ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [Measure.restrict_smul, lintegral_smul_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν
have 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 ν)
Tactic: simp only [lintegral, SimpleFunc.lintegral_add, iSup_subtype']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ν)
have 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 ν
Tactic: refine (ENNReal.iSup_add_iSup ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ν
have 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) (φ ⊔ ψ)
              sorry) :
          α →ₛ ℝ≥0∞).lintegral
      μ +
    (↑(Subtype.mk (p := fun (i : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a)
              (φ ⊔ ψ) sorry) :
          α →ₛ ℝ≥0∞).lintegral
      ν
Tactic: refine ⟨⟨φ ⊔ ψ, sup_le hφ hψ⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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
⊢ (↑(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
        ν
have h₁ : φ ≤ φ ⊔ ψ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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₁ : φ ≤ φ ⊔ ψ
⊢ (↑(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
        ν
have h₂ : ψ ≤ φ ⊔ ψ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_4
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
have simp_rw : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∑ i ∈ s, ∫⁻ (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 ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
have simp_rw₁ : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∫⁻ (a : α), f a ∂∑ i ∈ s, μ 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 ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
have 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))
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 ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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))
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
have 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))
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 ι)]