awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have μ'D : μ' D = 0 := by
    rcases eventually_iff_exists_mem.1 hc with ⟨V, ae, hV⟩
    exact eq_of_le_of_not_lt (mem_ae_iff.1 ae ▸ (μ'.mono <| fun x h xV ↦ h.2 (hV x xV)))
      _root_.not_lt_zero
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [μ'D]
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (U : Set (ι → ℝ)) (UD : U ⊇ D) (Uopen : IsOpen U)
    (hU :
      (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U <
        HAdd.hAdd (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (ENNReal.ofReal ε₂)),
    ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
      (∀ (c : ℝ≥0), l.RCond (r c)) ∧
        ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
          l.MemBaseSet I c₁ (r c₁) π₁ →
            π₁.IsPartition →
              l.MemBaseSet I c₂ (r c₂) π₂ →
                π₂.IsPartition →
                  dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε

Tactic:
obtain ⟨U, UD, Uopen, hU⟩ := Set.exists_isOpen_lt_add D (show μ' D ≠ ⊤ by simp [μ'D]) ε₂0'

Premises used: Set.exists_isOpen_lt_add
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU :
  (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U <
    HAdd.hAdd (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (ENNReal.ofReal ε₂)
⊢ (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂

Tactic:
rw [μ'D, zero_add] at hU

Premises used: zero_add
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
⊢ IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)

Tactic:
have comp : IsCompact (Box.Icc I \ U) :=
    I.isCompact_Icc.of_isClosed_subset (I.isCompact_Icc.isClosed.sdiff Uopen) Set.diff_subset
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x
this : oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x = 0
rw : 0 < ENNReal.ofReal ε₁
⊢ oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁

Tactic:
rw [this]
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x
this : oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x = 0
⊢ 0 < ENNReal.ofReal ε₁

Tactic:
ofReal_pos.2 ε₁0

Premises used: Iff.mpr, ENNReal.ofReal_pos
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x
this : oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x = 0
⊢ 0 < ENNReal.ofReal ε₁

Tactic:
exact ofReal_pos.2 ε₁0

Premises used: Iff.mpr, ENNReal.ofReal_pos
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x
suffices : oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x = 0
⊢ oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁

Tactic:
suffices oscillationWithin f (Box.Icc I) x = 0 by rw [this]; exact ofReal_pos.2 ε₁0
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x
⊢ oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x = 0

Tactic:
simpa [OscillationWithin.eq_zero_iff_continuousWithinAt, D, hx.1] using hx.2 ∘ (fun a ↦ UD a)

Premises used: And.right, And.left, OscillationWithin.eq_zero_iff_continuousWithinAt
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
⊢ ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁

Tactic:
have : ∀ x ∈ (Box.Icc I \ U), oscillationWithin f (Box.Icc I) x < (ENNReal.ofReal ε₁) := by
    intro x hx
    suffices oscillationWithin f (Box.Icc I) x = 0 by rw [this]; exact ofReal_pos.2 ε₁0
    simpa [OscillationWithin.eq_zero_iff_continuousWithinAt, D, hx.1] using hx.2 ∘ (fun a ↦ UD a)
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
rcases :
  ∀ (r : ℝ) (r0 : r > 0)
    (hr :
      ∀ (x : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
          ediam (f '' (eball x (ENNReal.ofReal r) ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) ≤ ENNReal.ofReal ε₁),
    ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
      (∀ (c : ℝ≥0), l.RCond (r c)) ∧
        ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
          l.MemBaseSet I c₁ (r c₁) π₁ →
            π₁.IsPartition →
              l.MemBaseSet I c₂ (r c₂) π₂ →
                π₂.IsPartition →
                  dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε

Tactic:
rcases comp.uniform_oscillationWithin this with ⟨r, r0, hr⟩

Premises used: IsCompact.uniform_oscillationWithin
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      ediam (f '' (eball x (ENNReal.ofReal r) ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) ≤ ENNReal.ofReal ε₁
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε

Tactic:
⟨fun _ _ ↦ ⟨r / 2, half_pos r0⟩, fun _ _ _ ↦ rfl, fun c₁ c₂ π₁ π₂ h₁ h₁p h₂ h₂p ↦ ?_⟩

Premises used: half_pos, HDiv.hDiv, Subtype.mk, And.intro, Exists.intro, OfNat.ofNat, rfl