awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
rw :
  ∀
    (hf :
      @Integrable _ _ _ { x : X // x ∈ s } (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
        (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
      (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
⊢ @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
have hg : ∀
  (hf :
    @Integrable _ _ _ _ mX f
      (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)))
  (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
  AEStronglyMeasurable (m₀ := mX) f
    (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
Tactic: rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf
Cleared hypotheses: hf, hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
rw :
  ∀
    (hf :
      @Integrable _ _ _ { x : X // x ∈ s } (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
        (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
      (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
hg :
  ∀
    (hf :
      @Integrable _ _ _ _ mX f
        (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
          (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    AEStronglyMeasurable (m₀ := mX) f
      (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
⊢ @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
have hf₁ : ∀
  (hf :
    @Integrable _ _ _ _ mX f
      (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)))
  (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
  AEMeasurable (α := { x : X // x ∈ s }) (_m := Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
Tactic: rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf
Cleared hypotheses: hf, hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
rw :
  ∀
    (hf :
      @Integrable _ _ _ { x : X // x ∈ s } (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
        (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
      (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
hg :
  ∀
    (hf :
      @Integrable _ _ _ _ mX f
        (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
          (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    AEStronglyMeasurable (m₀ := mX) f
      (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
hf₁ :
  ∀
    (hf :
      @Integrable _ _ _ _ mX f
        (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
          (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    AEMeasurable (α := { x : X // x ∈ s }) (_m := Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
      (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
⊢ @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
have hs₁ : ∀ (hf : Integrable f (μ.restrict s)) (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }), MeasurableSet s
Tactic: rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf
Cleared hypotheses: hf, hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∑' (x : (↑s : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
have hf' : @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
  (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
Tactic: have hf' : Integrable (fun (x : s) ↦ f x) (Measure.comap Subtype.val μ) := by
    rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf
    · apply hf
    · exact Integrable.aestronglyMeasurable hf
    · exact Measurable.aemeasurable measurable_subtype_coe
    · exact Countable.measurableSet hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
hf' :
  @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∑' (x : (↑s : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
have rw : Eq.{u_3 + 1} (α := E)
  (∑' (x : (↑s : Type u_2)),
    Measure.real (α := (↑s : Type u_2)) (m := Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) {x} •
      f (↑x : X))
  (∑' (x : (↑s : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
Tactic: rw [← integral_subtype_comap hs.measurableSet, integral_countable hf']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
hf' :
  @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
⊢ Eq.{u_3 + 1} (α := E)
    (∑' (x : (↑s : Type u_2)),
      Measure.real (α := (↑s : Type u_2)) (m := Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
          (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) {x} •
        f (↑x : X))
    (∑' (x : (↑s : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
have e_f : ∀ (a : (↑s : Type u_2)),
  Measure.real (α := (↑s : Type u_2)) (m := Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) {a} •
      f (↑a : X) =
    μ.real {(↑a : X)} • f (↑a : X)
Tactic: congr 1 with a : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
hf' :
  @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
a : (↑s : Type u_2)
⊢ Measure.real (α := (↑s : Type u_2)) (m := Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) {a} •
      f (↑a : X) =
    μ.real {(↑a : X)} • f (↑a : X)
have e_f : ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) {a})) •
    f (↑a : X) =
  μ.real {(↑a : X)} • f (↑a : X)
Tactic: rw [measureReal_def, Measure.comap_apply Subtype.val Subtype.coe_injective
    (fun s' hs' ↦ MeasurableSet.subtype_image (Countable.measurableSet hs) hs') _
    (MeasurableSet.singleton a)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
s : Finset X
hf : IntegrableOn f (↑s : Set X) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in (↑s : Set X), f x ∂μ) (∑ x ∈ s, μ.real {x} • f x)
have rw : Eq.{u_3 + 1} (α := E) (∑' (x : (↑(↑s : Set X) : Type u_2)), μ.real {(↑x : X)} • f (↑x : X)) (∑ x ∈ s, μ.real {x} • f x)
Tactic: rw [setIntegral_countable _ s.countable_toSet hf, ← Finset.tsum_subtype']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
s : Finset X
hf : IntegrableOn f (↑s : Set X) μ
rw :
  Eq.{u_3 + 1} (α := E) (∑' (x : (↑(↑s : Set X) : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
    (∑ x ∈ s, μ.real {x} • f x)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in (↑s : Set X), f x ∂μ) (∑ x ∈ s, μ.real {x} • f x)
have rw₁ : Eq.{u_3 + 1} (α := E) (∑' (x : (↑(↑s : Set X) : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
  (∑' (x : (↑(↑s : Set X) : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
Tactic: rw [setIntegral_countable _ s.countable_toSet hf, ← Finset.tsum_subtype']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
inst_4 : Fintype X
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∑ x : X, μ.real {x} • f x)
have rw : IntegrableOn f (↑Finset.univ : Set X) μ
Tactic: rw [← setIntegral_finset .univ, Finset.coe_univ, Measure.restrict_univ]
-- 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)
⊢ ∃ (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 pos : ∀ (h : ∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) 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∞) ∂μ + ε
Tactic: by_cases h : ∫⁻ x, f x ∂μ = ⊤
-- 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)
pos :
  ∀ (h : ∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) 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∞) ∂μ + ε
⊢ ∃ (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 : ∀ (h : ¬∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) 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∞) ∂μ + ε
Tactic: by_cases h : ∫⁻ x, f x ∂μ = ⊤
-- 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∞) ∂μ = ∞
⊢ ∃ (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 pos : ∀ (x : α),
  LE.le (α := ℝ≥0) ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0) ((fun (x : α) ↦ c) x : ℝ≥0)
Tactic: refine
        ⟨fun _ => c, fun x => ?_, lowerSemicontinuous_const, by
          simp only [f, _root_.top_add, le_top, h]⟩
-- 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∞) ∂μ = ∞
x : α
⊢ LE.le (α := ℝ≥0) ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0) ((fun (x : α) ↦ c) x : ℝ≥0)
have pos : s.indicator (Function.const α c) x ≤ c
Tactic: simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise]
-- 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∞) ∂μ = ∞
⊢ ∃ (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 pos : ∀ (hc : 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: by_cases hc : c = 0
-- 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∞) ∂μ = ∞
pos :
  ∀ (hc : 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∞) ∂μ + ε
⊢ ∃ (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 : ∀ (hc : ¬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: by_cases hc : c = 0
-- 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
⊢ ∃ (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 pos : ∀ (x : α),
  LE.le (α := ℝ≥0) ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
    ((fun (x : α) ↦ (0 : ℝ≥0)) x : ℝ≥0)
Tactic: refine ⟨fun _ => 0, ?_, lowerSemicontinuous_const, ?_⟩
-- 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
pos :
  ∀ (x : α),
    LE.le (α := ℝ≥0) ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
      ((fun (x : α) ↦ (0 : ℝ≥0)) 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 pos₁ : ∫⁻ (x : α), (↑((fun (x : α) ↦ (0 : ℝ≥0)) x) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
Tactic: refine ⟨fun _ => 0, ?_, lowerSemicontinuous_const, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
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
⊢ ∃ (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 ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have ne_top : μ s ≠ ⊤ := by
      classical
      simpa [f, hs, hc, lt_top_iff_ne_top, SimpleFunc.coe_const,
        Function.const_apply, lintegral_const, ENNReal.coe_indicator, Set.univ_inter,
        ENNReal.coe_ne_top, MeasurableSet.univ, ENNReal.mul_eq_top, SimpleFunc.const_zero,
        lintegral_indicator, ENNReal.coe_eq_zero, Ne, not_false_iff,
        SimpleFunc.coe_zero, Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise,
        restrict_apply] using h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
have this : 0 < ε / (↑c : ℝ≥0∞)
Tactic: have : (0 : ℝ≥0∞) < ε / c := ENNReal.div_pos_iff.2 ⟨ε0, ENNReal.coe_ne_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
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∞)
⊢ ∃ (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 this : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
Tactic: have : μ s < μ s + ε / c := by
      have : (0 : ℝ≥0∞) < ε / c := ENNReal.div_pos_iff.2 ⟨ε0, ENNReal.coe_ne_top⟩
      simpa using ENNReal.add_lt_add_left ne_top this