awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have neg : ∀ (u : Set α) (su : u ⊇ s) (u_open : IsOpen u)
  (μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
Tactic: obtain ⟨u, su, u_open, μu⟩ : ∃ (u : _), u ⊇ s ∧ IsOpen u ∧ μ u < μ s + ε / c :=
      s.exists_isOpen_lt_of_lt _ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have neg : ∀ (x : α),
  LE.le (α := ℝ≥0) ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
    (u.indicator (fun (x : α) ↦ c) x : ℝ≥0)
Tactic: refine ⟨Set.indicator u fun _ => c,
      fun x => ?_, u_open.lowerSemicontinuous_indicator zero_le, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
neg :
  ∀ (x : α),
    LE.le (α := ℝ≥0) ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
      (u.indicator (fun (x : α) ↦ c) x : ℝ≥0)
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have neg₁ : ∫⁻ (x : α), (↑(u.indicator (fun (x : α) ↦ c) x) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
Tactic: refine ⟨Set.indicator u fun _ => c,
      fun x => ?_, u_open.lowerSemicontinuous_indicator zero_le, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
x : α
⊢ LE.le (α := ℝ≥0) ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
    (u.indicator (fun (x : α) ↦ c) x : ℝ≥0)
have neg : LE.le (α := ℝ≥0) (s.indicator (fun (x : α) ↦ c) x) (u.indicator (fun (x : α) ↦ c) x)
Tactic: simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, ← Function.const_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
x : α
⊢ LE.le (α := ℝ≥0) (s.indicator (fun (x : α) ↦ c) x) (u.indicator (fun (x : α) ↦ c) x)
have h₂ : 0 ≤ c
Tactic: grw [su]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
x : α
h₂ : 0 ≤ c
⊢ LE.le (α := ℝ≥0) (s.indicator (fun (x : α) ↦ c) x) (u.indicator (fun (x : α) ↦ c) x)
have neg : LE.le (α := ℝ≥0) (s.indicator (fun (x : α) ↦ c) x) (s.indicator (fun (x : α) ↦ c) x)
Tactic: grw [su]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ ∫⁻ (x : α), (↑(u.indicator (fun (x : α) ↦ c) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have neg : HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε
Tactic: suffices (c : ℝ≥0∞) * μ u ≤ c * μ s + ε by
        classical
        simpa only [ENNReal.coe_indicator, u_open.measurableSet, lintegral_indicator,
          lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, const_zero,
          coe_piecewise, coe_const, coe_zero, Set.piecewise_eq_indicator, Function.const_apply, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ≤
    (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
have grw : (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞)) ≤
  (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
Tactic: grw [μu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞)) =
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε
have simp_rw : HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + (↑c : ℝ≥0∞) * (ε / (↑c : ℝ≥0∞)) =
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε
Tactic: simp_rw [mul_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + (↑c : ℝ≥0∞) * (ε / (↑c : ℝ≥0∞)) =
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε
have rw : (↑c : ℝ≥0∞) ≠ 0
Tactic: rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε
have μ₁ : HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ≤
  (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
Tactic: calc
        (c : ℝ≥0∞) * μ u ≤ c * (μ s + ε / c) := by grw [μu]
        _ = c * μ s + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∞
hc : ¬c = 0
ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : (μ : (a : Set α) → ℝ≥0∞) u < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
μ₁ :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ≤
    (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε
have μ₂ : (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞)) =
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε
Tactic: calc
        (c : ℝ≥0∞) * μ u ≤ c * (μ s + ε / c) := by grw [μu]
        _ = c * μ s + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have add : ∀ (g₁ : α → ℝ≥0) (f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x) (g₁cont : LowerSemicontinuous g₁)
  (g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases h₁ (ENNReal.half_pos ε0).ne' with ⟨g₁, f₁_le_g₁, g₁cont, g₁int⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have add : ∀ (g₂ : α → ℝ≥0) (f₂_le_g₂ : ∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g₂ x) (g₂cont : LowerSemicontinuous g₂)
  (g₂int : ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases h₂ (ENNReal.half_pos ε0).ne' with ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have add : ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
Tactic: refine
      ⟨fun x => g₁ x + g₂ x, fun x => add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have add : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
Tactic: simp only [SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
have add : ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε
Tactic: rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
      lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal]