awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x
hs : x ∈ s
⊢ ‖F x‖ ≤ max 0 C₀

Tactic:
exact le_max_of_le_right (h₀ x hx)

Premises used: le_max_of_le_right
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x
hs : x ∉ s
⊢ norm (E := ℝ) 0 ≤ max 0 C₀

Tactic:
norm_zero.trans_le <| le_max_left 0 _

Premises used: norm_zero, Eq.trans_le, OfNat.ofNat, le_max_left
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x
hs : x ∉ s
⊢ norm (E := ℝ) 0 ≤ max 0 C₀

Tactic:
exact norm_zero.trans_le <| le_max_left 0 _

Premises used: norm_zero, Eq.trans_le, OfNat.ofNat, le_max_left
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C

Tactic:
have h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖Set.indicator s F x‖ ≤ C := by
    obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn
    refine ⟨max 0 C₀, fun x hx ↦ ?_⟩
    rw [Set.indicator]
    split_ifs with hs
    · exact le_max_of_le_right (h₀ x hx)
    · exact norm_zero.trans_le <| le_max_left 0 _
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
a : ι → ℝ
h : a ∈ (frontier s)ᶜ
⊢ ContinuousAt (s.indicator F) a

Tactic:
(hF.continuousOn).continuousAt_indicator h

Premises used: ContinuousOn.continuousAt_indicator, Continuous.continuousOn
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h :
  ∀ (a : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ))
      {x : ι → ℝ |
        x ∈ (frontier s)ᶜ →
          Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | (fun (x : ι → ℝ) ↦ ContinuousAt (s.indicator F) x) x} x}
      a
h₂ h₃ : ∀ (a : ι → ℝ) (h : a ∈ (frontier s)ᶜ), ContinuousAt (s.indicator F) a
⊢ ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x

Tactic:
filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h
      using (hF.continuousOn).continuousAt_indicator h

Premises used: Iff.mpr, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
⊢ ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x

Tactic:
have h₂ : ∀ᵐ x, ContinuousAt (s.indicator F) x := by
    filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h
      using (hF.continuousOn).continuousAt_indicator h
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
obtain :
  ∀ (r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) (hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c))
    (hr₂ :
      ∀ (c : NNReal) (π : TaggedPrepartition B),
        IntegrationParams.Riemann.MemBaseSet B c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
                (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
                  (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
              ε / 2),
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((∑' (x :
                (↑(s ∩
                      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                  Type u_1)),
                F (↑x : ι → ℝ)) /
              HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
            (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s)
              fun (x : ι → ℝ) ↦ F x) <
          ε
⊢ ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε

Tactic:
obtain ⟨r, hr₁, hr₂⟩ := (hasIntegral_iff.mp <|
      AEContinuous.hasBoxIntegral (volume : Measure (ι → ℝ)) h₁ h₂
        IntegrationParams.Riemann) (ε / 2) (half_pos hε)

Premises used: half_pos, MeasureTheory.AEContinuous.hasBoxIntegral, HDiv.hDiv, MeasureTheory.MeasureSpace.volume, Iff.mp, BoxIntegral.hasIntegral_iff, OfNat.ofNat, BoxIntegral.IntegrationParams.Riemann
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
⊢ ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε

Tactic:
⟨⌈(r 0 0 : ℝ)⁻¹⌉₊, fun n hn ↦ lt_of_le_of_lt ?_ (half_lt_self_iff.mpr hε)⟩

Premises used: Iff.mpr, lt_of_le_of_lt, half_lt_self_iff, Inv.inv, Nat.ceil, Exists.intro, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
refine :
  ∀ (n : ℕ) (hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊),
    dist
        ((∑' (x :
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)),
            F (↑x : ι → ℝ)) /
          HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
        (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
          F x) ≤
      ε / 2
⊢ ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε

Tactic:
refine ⟨⌈(r 0 0 : ℝ)⁻¹⌉₊, fun n hn ↦ lt_of_le_of_lt ?_ (half_lt_self_iff.mpr hε)⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
⊢ NeZero n

Tactic:
have : NeZero n :=
    ⟨Nat.ne_zero_iff_zero_lt.mpr <| (Nat.ceil_pos.mpr (inv_pos.mpr (r 0 0).prop)).trans_le hn⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
rw :
  dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
      (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
        (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
    ε / 2
⊢ dist
      ((∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x) ≤
    ε / 2

Tactic:
rw [← integralSum_eq_tsum_div _ s F hB hs₀, ← Measure.restrict_restrict_of_subset hs₀,
    ← integral_indicator hs₂]

Premises used: MeasureTheory.integral_indicator, BoxIntegral.unitPartition.integralSum_eq_tsum_div, MeasureTheory.Measure.restrict_restrict_of_subset
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
⊢ dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
      (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
        (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
    ε / 2

Tactic:
hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB)

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.mk, BoxIntegral.unitPartition.prepartition_isPartition, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
refine_1 : (prepartition n B).IsSubordinate (r 0)
refine_2 : IntegrationParams.Riemann.bHenstock = true → (prepartition n B).IsHenstock
refine_3 : ∀ (h : IntegrationParams.Riemann.bDistortion = true), (prepartition n B).distortion ≤ 0
refine_4 :
  ∀ (h : IntegrationParams.Riemann.bDistortion = true),
    ∃ (π' : Prepartition B), π'.iUnion = (↑B : Set (ι → ℝ)) \ (prepartition n B).iUnion ∧ π'.distortion ≤ 0
⊢ dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
      (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
        (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
    ε / 2

Tactic:
refine hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB)

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.mk, BoxIntegral.unitPartition.prepartition_isPartition, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
refine_1 : (prepartition n B).IsSubordinate fun (x : ι → ℝ) ↦ r 0 0
⊢ (prepartition n B).IsSubordinate (r 0)

Tactic:
rw [show r 0 = fun _ ↦ r 0 0 from funext_iff.mpr (hr₁ 0 rfl)]

Premises used: Iff.mpr, funext_iff, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
refine_1 : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑(r 0 0) : ℝ)
⊢ (prepartition n B).IsSubordinate fun (x : ι → ℝ) ↦ r 0 0

Tactic:
apply prepartition_isSubordinate n B

Premises used: BoxIntegral.unitPartition.prepartition_isSubordinate
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
refine_1 : (↑(r 0 0) : ℝ)⁻¹ ≤ (↑n : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑(r 0 0) : ℝ)

Tactic:
rw [one_div, inv_le_comm₀ (mod_cast (Nat.pos_of_neZero n)) (r 0 0).prop]

Premises used: inv_le_comm₀, one_div