awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have refine : ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π) (hπp : π.IsPartition),
  dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
    ‖y‖ * (↑ε : ℝ)
Tactic: refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ hπp => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
⊢ dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
    ‖y‖ * (↑ε : ℝ)
have rw : dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
  (↑ε : ℝ) * ‖y‖
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
⊢ dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
    (↑ε : ℝ) * ‖y‖
have dsimp : dist (∑ J ∈ π.boxes, HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) (s.indicator (fun (x : ι → ℝ) ↦ y) (π.tag J)))
    (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
  (↑ε : ℝ) * ‖y‖
Tactic: dsimp [integralSum]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
⊢ dist (∑ J ∈ π.boxes, HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) (s.indicator (fun (x : ι → ℝ) ↦ y) (π.tag J)))
      (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
    (↑ε : ℝ) * ‖y‖
have simp : |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| * ‖y‖ ≤ (↑ε : ℝ) * ‖y‖
Tactic: simp only [dist_eq_norm, ← indicator_const_smul_apply, sum_indicator_eq_sum_filter, ← sum_smul,
    ← sub_smul, norm_smul, Real.norm_eq_abs, ← Prepartition.filter_boxes,
    ← Prepartition.measure_iUnion_toReal]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
⊢ |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| * ‖y‖ ≤ (↑ε : ℝ) * ‖y‖
have hbc : |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
⊢ |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
have hbc : |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
Tactic: change abs (μ.real t - μ.real (s ∩ I)) ≤ ε
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
⊢ t ⊆ U ∩ (↑I : Set (ι → ℝ))
have simp : ∀ i ∈ π, π.tag i ∈ s → (↑i : Set (ι → ℝ)) ⊆ U ∩ (↑I : Set (ι → ℝ))
Tactic: simp only [t, TaggedPrepartition.iUnion_def, iUnion_subset_iff, TaggedPrepartition.mem_filter,
      and_imp]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
⊢ ∀ i ∈ π, π.tag i ∈ s → (↑i : Set (ι → ℝ)) ⊆ U ∩ (↑I : Set (ι → ℝ))
have refine : ∀ (J : Box ι) (hJ : J ∈ π) (hJs : π.tag J ∈ s) (x : ι → ℝ) (hx : x ∈ (↑J : Set (ι → ℝ))),
  x ∈ closedBall (π.tag J) (↑(rs (π.tag J)) : ℝ)
Tactic: refine fun J hJ hJs x hx => ⟨hrsU _ ⟨hJs, π.tag_mem_Icc J⟩ ?_, π.le_of_mem' J hJ hx⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
⊢ |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
have htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
Tactic: have htU : t ⊆ U ∩ I := by
    simp only [t, TaggedPrepartition.iUnion_def, iUnion_subset_iff, TaggedPrepartition.mem_filter,
      and_imp]
    refine fun J hJ hJs x hx => ⟨hrsU _ ⟨hJs, π.tag_mem_Icc J⟩ ?_, π.le_of_mem' J hJ hx⟩
    simpa only [r, s.piecewise_eq_of_mem _ _ hJs] using hπ.1 J hJ (Box.coe_subset_Icc hx)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
⊢ |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
have hbc : μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ))) ≤ (↑ε : ℝ)
Tactic: refine abs_sub_le_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hbc : μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ))) ≤ (↑ε : ℝ)
⊢ |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
have hbc₁ : μ.real (s ∩ (↑I : Set (ι → ℝ))) - μ.real t ≤ (↑ε : ℝ)
Tactic: refine abs_sub_le_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrs'F :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
⊢ μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ))) ≤ (↑ε : ℝ)
have hbc : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) ≤
  (↑ε : ℝ≥0∞)
Tactic: refine (ENNReal.le_toReal_sub B).trans (ENNReal.toReal_le_coe_of_le_coe ?_)