awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
dsimp :
  dist (∑ J ∈ π.boxes, HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) (s.indicator (fun (x : ι → ℝ) ↦ y) (π.tag J)))
      (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
    (↑ε : ℝ) * ‖y‖
⊢ dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
    (↑ε : ℝ) * ‖y‖

Tactic:
dsimp [integralSum]

Premises used: BoxIntegral.integralSum
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
simp : |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| * ‖y‖ ≤ (↑ε : ℝ) * ‖y‖
⊢ dist (∑ J ∈ π.boxes, HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) (s.indicator (fun (x : ι → ℝ) ↦ y) (π.tag J)))
      (μ.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]

Premises used: BoxIntegral.Prepartition.measure_iUnion_toReal, Finset.sum_smul, dist_eq_norm, norm_smul, BoxIntegral.Prepartition.filter_boxes, sub_smul, Finset.sum_indicator_eq_sum_filter, Set.indicator_const_smul_apply, Real.norm_eq_abs
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
hbc : |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
⊢ |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| * ‖y‖ ≤ (↑ε : ℝ) * ‖y‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
hbc : |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)
⊢ |μ.real (π.filter fun (i : Box ι) ↦ π.tag i ∈ s).iUnion - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)

Tactic:
change abs (μ.real t - μ.real (s ∩ I)) ≤ ε

Premises used: abs, BoxIntegral.Box.toSet, MeasureTheory.Measure.real, HSub.hSub, Inter.inter
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
simp : ∀ i ∈ π, π.tag i ∈ s → (↑i : Set (ι → ℝ)) ⊆ U ∩ (↑I : Set (ι → ℝ))
⊢ t ⊆ U ∩ (↑I : Set (ι → ℝ))

Tactic:
simp only [t, TaggedPrepartition.iUnion_def, iUnion_subset_iff, TaggedPrepartition.mem_filter,
      and_imp]

Premises used: Set.iUnion_subset_iff, and_imp, BoxIntegral.TaggedPrepartition.mem_filter, BoxIntegral.TaggedPrepartition.iUnion_def
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 (ι → ℝ))

Tactic:
fun J hJ hJs x hx => ⟨hrsU _ ⟨hJs, π.tag_mem_Icc J⟩ ?_, π.le_of_mem' J hJ hx⟩

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc, Set.Mem, setOf, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.TaggedPrepartition.tag, Set.inter, Set.Subset, And.intro, BoxIntegral.Prepartition.le_of_mem'
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
refine :
  ∀ (J : Box ι) (hJ : J ∈ π) (hJs : π.tag J ∈ s) (x : ι → ℝ) (hx : x ∈ (↑J : Set (ι → ℝ))),
    x ∈ closedBall (π.tag J) (↑(rs (π.tag J)) : ℝ)
⊢ ∀ i ∈ π, π.tag i ∈ s → (↑i : Set (ι → ℝ)) ⊆ U ∩ (↑I : Set (ι → ℝ))

Tactic:
refine fun J hJ hJs x hx => ⟨hrsU _ ⟨hJs, π.tag_mem_Icc J⟩ ?_, π.le_of_mem' J hJ hx⟩
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
J : Box ι
hJ : J ∈ π
hJs : π.tag J ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
⊢ x ∈ closedBall (π.tag J) (↑(rs (π.tag J)) : ℝ)

Tactic:
simpa only [r, s.piecewise_eq_of_mem _ _ hJs] using hπ.1 J hJ (Box.coe_subset_Icc hx)

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate, Set.piecewise_eq_of_mem, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 (ι → ℝ))

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)
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 (ι → ℝ)))| ≤ (↑ε : ℝ)

Tactic:
abs_sub_le_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_sub_le_iff, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 (ι → ℝ))) ≤ (↑ε : ℝ)
hbc₁ : μ.real (s ∩ (↑I : Set (ι → ℝ))) - μ.real t ≤ (↑ε : ℝ)
⊢ |μ.real t - μ.real (s ∩ (↑I : Set (ι → ℝ)))| ≤ (↑ε : ℝ)

Tactic:
refine abs_sub_le_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_sub_le_iff, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 (ι → ℝ))) ≤ (↑ε : ℝ)

Tactic:
(ENNReal.le_toReal_sub B).trans (ENNReal.toReal_le_coe_of_le_coe ?_)

Premises used: ENNReal.le_toReal_sub, MeasureTheory.Measure.real, ENNReal.toReal_le_coe_of_le_coe, LE.le.trans