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)
μ'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_1 :
  ∀ (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 ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ :
  l.MemBaseSet I c₁
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₁)
    π₁
h₁p : π₁.IsPartition
h₂ :
  l.MemBaseSet I c₂
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₂)
    π₂
h₂p : π₂.IsPartition
μI : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : (J : Box ι) → ι → ℝ := fun (J : Box ι) ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : (J : Box ι) → ι → ℝ := fun (J : Box ι) ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | (↑J : Set (ι → ℝ)) ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑J : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)
un : ∀ S ⊆ B, ⋃ J ∈ S, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))
this :
  ∀ J ∈ B',
    ‖HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) J : ℝ) (f (t₁ J) - f (t₂ J))‖ ≤
      HMul.hMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) J : ℝ) (2 * C)
⊢ ∀ (i : Box ι) (i_1 : i ∈ B'), (↑i : Set (ι → ℝ)) ⊆ U

Tactic:
exact fun J hJ ↦ (mem_filter.1 hJ).2

Premises used: And.right, Iff.mp, Finset.mem_filter
-- 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
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
⊢ Integrable I l f μ.toBoxAdditive.toSMul

Tactic:
integrable_of_bounded_and_ae_continuousWithinAt l hb μ <|
    Eventually.filter_mono (ae_mono μ.restrict_le_self) (hc.mono fun _ h ↦ h.continuousWithinAt)

Premises used: Filter.Eventually.filter_mono, ContinuousAt.continuousWithinAt, MeasureTheory.ae_mono, Filter.Eventually.mono, MeasureTheory.Measure.restrict_le_self, BoxIntegral.integrable_of_bounded_and_ae_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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc₁ :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
⊢ Integrable I l f μ.toBoxAdditive.toSMul

Tactic:
apply integrable_of_bounded_and_ae_continuousWithinAt

Premises used: BoxIntegral.integrable_of_bounded_and_ae_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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hb :
  ∀ (C : ℝ) (hC : f '' (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ HSMul.hSMul (β := Set E) C (Metric.closedBall 0 1)),
    ∃ (C : ℝ),
      ∀ (x : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C

Tactic:
obtain ⟨C, hC⟩ := (NormedSpace.isBounded_iff_subset_smul_closedBall ℝ).1
                        (I.isCompact_Icc.image_of_continuousOn hc).isBounded

Premises used: Real, IsCompact.isBounded, NormedSpace.isBounded_iff_subset_smul_closedBall, BoxIntegral.Box.isCompact_Icc, IsCompact.image_of_continuousOn, Iff.mp
-- 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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ
hC : f '' (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ HSMul.hSMul (β := Set E) C (Metric.closedBall 0 1)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
⊢ ‖f x‖ ≤ ‖C‖

Tactic:
simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)

Premises used: smul_unitClosedBall, Set.mem_image_of_mem, mem_closedBall_zero_iff
-- 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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ
hC : f '' (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ HSMul.hSMul (β := Set E) C (Metric.closedBall 0 1)
w : ℝ
h :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ ‖C‖
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C

Tactic:
use ‖C‖, fun x hx ↦ by
      simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)
-- 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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
⊢ ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x

Tactic:
eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)

Premises used: Filter.eventually_of_mem, ContinuousOn.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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc₁ :
  Membership.mem (α := Set (ι → ℝ)) (ae (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)))
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
⊢ ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x

Tactic:
refine eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)

Premises used: Filter.eventually_of_mem, ContinuousOn.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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc₁ :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞)
        (((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)ᶜ ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
hc₂ : MeasurableSet.{u} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)ᶜ
⊢ Membership.mem (α := Set (ι → ℝ)) (ae (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)))
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))

Tactic:
rw [mem_ae_iff, μ.restrict_apply]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.mem_ae_iff
-- 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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞)
        (((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)ᶜ ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [MeasurableSet.compl_iff.2 I.measurableSet_Icc]

Premises used: Iff.mpr, BoxIntegral.Box.measurableSet_Icc, MeasurableSet.compl_iff
-- 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
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
⊢ MeasurableSet.{u} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)ᶜ

Tactic:
simp [MeasurableSet.compl_iff.2 I.measurableSet_Icc]

Premises used: Iff.mpr, BoxIntegral.Box.measurableSet_Icc, MeasurableSet.compl_iff
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
H₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
H₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
⊢ HasIntegral I l f vol ((g : (a : Box ι) → F) I)

Tactic:
((l.hasBasis_toFilteriUnion_top _).tendsto_iff Metric.nhds_basis_closedBall).2 ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top, Metric.nhds_basis_closedBall, BoxIntegral.HasIntegral
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
H₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
H₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
refine :
  ∀ (ib : ℝ),
    0 < ib →
      ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
          ∀ (x : TaggedPrepartition I),
            Membership.mem (γ := Set (TaggedPrepartition I))
                {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.IsPartition} x →
              Membership.mem (γ := Set F) (Metric.closedBall ((g : (a : Box ι) → F) I) ib : Set F) (integralSum f vol x)
⊢ HasIntegral I l f vol ((g : (a : Box ι) → F) I)

Tactic:
refine ((l.hasBasis_toFilteriUnion_top _).tendsto_iff Metric.nhds_basis_closedBall).2 ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
H₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
H₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε : ℝ
ε0 : 0 < ε
⊢ ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∃ (x_1 : { a : ℝ // 0 < a }),
            ∀ J ≤ I,
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑x_1 : ℝ) →
                Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                  (l.bDistortion = true → J.distortion ≤ c) →
                    dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                        ((g : (a : Box ι) → F) J : F) ≤
                      ε

Tactic:
simp only [← exists_prop, gt_iff_lt, Subtype.exists'] at H₁ H₂

Premises used: Subtype.exists', exists_prop, gt_iff_lt
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
⊢ 0 < ε / 2

Tactic:
have ε0' := half_pos ε0
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
⊢ 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)

Tactic:
have H0 : 0 < (2 : ℝ) ^ Fintype.card ι := pow_pos zero_lt_two _