awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
neg :
  ∀ (F : Set α) (Fs : F ⊆ s) (F_closed : IsClosed F)
    (μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε

Tactic:
obtain ⟨F, Fs, F_closed, μF⟩ : ∃ (F : _), F ⊆ s ∧ IsClosed F ∧ μ s < μ F + ε / c :=
      hs.exists_isClosed_lt_add μs_lt_top.ne this.ne'

Premises used: MeasurableSet.exists_isClosed_lt_add, LT.lt.ne', DFunLike.coe, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε

Tactic:
⟨Set.indicator F fun _ => c, fun x => ?_, F_closed.upperSemicontinuous_indicator zero_le,
        ?_⟩

Premises used: zero_le, Set.indicator, IsClosed.upperSemicontinuous_indicator, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
neg :
  ∀ (x : α),
    LE.le (α := ℝ≥0) (F.indicator (fun (x : α) ↦ c) x : ℝ≥0)
      ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
neg₁ :
  ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑(F.indicator (fun (x : α) ↦ c) x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε

Tactic:
refine
      ⟨Set.indicator F fun _ => c, fun x => ?_, F_closed.upperSemicontinuous_indicator zero_le,
        ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
x : α
neg : LE.le (α := ℝ≥0) (F.indicator (fun (x : α) ↦ c) x) (s.indicator (fun (x : α) ↦ c) x)
⊢ LE.le (α := ℝ≥0) (F.indicator (fun (x : α) ↦ c) x : ℝ≥0)
    ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, ← Function.const_def]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Function.const_def, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
x : α
h₁ : 0 ≤ c
neg neg₁ : LE.le (α := ℝ≥0) (s.indicator (fun (x : α) ↦ c) x) (s.indicator (fun (x : α) ↦ c) x)
⊢ LE.le (α := ℝ≥0) (F.indicator (fun (x : α) ↦ c) x) (s.indicator (fun (x : α) ↦ c) x)

Tactic:
grw [Fs]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
this :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + ε
⊢ ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑(F.indicator (fun (x : α) ↦ c) x) : ℝ≥0∞) ∂μ + ε

Tactic:
simpa only [hs, F_closed.measurableSet, SimpleFunc.coe_const, Function.const_apply,
          lintegral_const, ENNReal.coe_indicator, Set.univ_inter, MeasurableSet.univ,
          SimpleFunc.const_zero, lintegral_indicator, SimpleFunc.coe_zero,
          Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, Measure.restrict_apply]

Premises used: Function.const_apply, MeasureTheory.lintegral_const, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.Measure.restrict_apply, MeasureTheory.SimpleFunc.coe_zero, IsClosed.measurableSet, Set.univ_inter, MeasureTheory.lintegral_indicator, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const, MeasurableSet.univ, ENNReal.coe_indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
neg :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + ε
⊢ ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑(F.indicator (fun (x : α) ↦ c) x) : ℝ≥0∞) ∂μ + ε

Tactic:
suffices (c : ℝ≥0∞) * μ s ≤ c * μ F + ε by
        simpa only [hs, F_closed.measurableSet, SimpleFunc.coe_const, Function.const_apply,
          lintegral_const, ENNReal.coe_indicator, Set.univ_inter, MeasurableSet.univ,
          SimpleFunc.const_zero, lintegral_indicator, SimpleFunc.coe_zero,
          Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, Measure.restrict_apply]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
grw grw₁ :
  (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞)) ≤
    (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))

Tactic:
grw [μF]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
simp_rw :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + (↑c : ℝ≥0∞) * (ε / (↑c : ℝ≥0∞)) =
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + ε
⊢ (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞)) =
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + ε

Tactic:
simp_rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
rw : (↑c : ℝ≥0∞) ≠ 0
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + (↑c : ℝ≥0∞) * (ε / (↑c : ℝ≥0∞)) =
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + ε

Tactic:
rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]

Premises used: ENNReal.mul_div_cancel, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simpa using hc
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
μ₁ :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
μ₂ :
  (↑c : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞)) =
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + ε
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) + ε

Tactic:
calc
        (c : ℝ≥0∞) * μ s ≤ c * (μ F + ε / c) := by grw [μF]
        _ = c * μ F + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc

Premises used: ENNReal.ofNNReal, HDiv.hDiv, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≠ ∞
⊢ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞

Tactic:
rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.SimpleFunc.measurable, MeasureTheory.lintegral_add_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞

Tactic:
have A : ((∫⁻ x : α, f₁ x ∂μ) + ∫⁻ x : α, f₂ x ∂μ) ≠ ⊤ := by
      rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
add :
  ∀ (g₁ : α → ℝ≥0) (f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x) (g₁cont : UpperSemicontinuous g₁)
    (g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε

Tactic:
rcases h₁ (ENNReal.add_ne_top.1 A).1 (ENNReal.half_pos ε0).ne' with
      ⟨g₁, f₁_le_g₁, g₁cont, g₁int⟩

Premises used: LT.lt.ne', And.left, ENNReal.half_pos, Iff.mp, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
add :
  ∀ (g₂ : α → ℝ≥0) (f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x) (g₂cont : UpperSemicontinuous g₂)
    (g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε

Tactic:
rcases h₂ (ENNReal.add_ne_top.1 A).2 (ENNReal.half_pos ε0).ne' with
      ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩

Premises used: LT.lt.ne', And.right, ENNReal.half_pos, Iff.mp, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε

Tactic:
⟨fun x => g₁ x + g₂ x, fun x => add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, ?_⟩

Premises used: add_le_add, HAdd.hAdd, UpperSemicontinuous.add, And.intro, Exists.intro