awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 ε₁
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 (ι → ℝ))
J : Box ι
h : J ∈ B'
⊢ μ.real (↑J : Set (ι → ℝ)) * ‖f (t₁ J) - f (t₂ J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * (C + C)
have hbc : ‖f (t₁ J) - f (t₂ J)‖ ≤ C + C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 ε₁
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 (ι → ℝ))
J : Box ι
h : J ∈ B'
⊢ ‖f (t₁ J) - f (t₂ J)‖ ≤ C + C
have hbc : ‖f (t₁ J)‖ ≤ C
Tactic: apply norm_sub_le_of_le
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 ε₁
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 (ι → ℝ))
J : Box ι
h : J ∈ B'
hbc : ‖f (t₁ J)‖ ≤ C
⊢ ‖f (t₁ J) - f (t₂ J)‖ ≤ C + C
have hbc₁ : ‖f (t₂ J)‖ ≤ C
Tactic: apply norm_sub_le_of_le
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ B', (↑J : Set (ι → ℝ))) : ℝ≥0∞)
    ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞)
have apply : ⋃ J ∈ B', (↑J : Set (ι → ℝ)) ⊆ U
Tactic: apply μ'.mono
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ ⋃ J ∈ B', (↑J : Set (ι → ℝ)) ⊆ U
have simp_rw : ∀ (i : Box ι) (i_1 : i ∈ B'), (↑i : Set (ι → ℝ)) ⊆ U
Tactic: simp_rw [iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 μ
⊢ Integrable I l f μ.toBoxAdditive.toSMul
have hb : ∃ (C : ℝ),
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
Tactic: apply integrable_of_bounded_and_ae_continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ Integrable I l f μ.toBoxAdditive.toSMul
have hc₁ : ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
  ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
Tactic: apply integrable_of_bounded_and_ae_continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
have 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
Tactic: obtain ⟨C, hC⟩ := (NormedSpace.isBounded_iff_subset_smul_closedBall ℝ).1
                        (I.isCompact_Icc.image_of_continuousOn hc).isBounded
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 : ℝ
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
have h : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
have hc₁ : Membership.mem (α := Set (ι → ℝ)) (ae (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)))
  ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
Tactic: refine eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 μ
⊢ Membership.mem (α := Set (ι → ℝ)) (ae (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)))
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
have hc₁ : Eq (α := ℝ≥0∞)
  ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞)
      (((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)ᶜ ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [mem_ae_iff, μ.restrict_apply]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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∞)
⊢ Membership.mem (α := Set (ι → ℝ)) (ae (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)))
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
have hc₂ : MeasurableSet.{u} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)ᶜ
Tactic: rw [mem_ae_iff, μ.restrict_apply]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
have 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)
Tactic: refine ((l.hasBasis_toFilteriUnion_top _).tendsto_iff Metric.nhds_basis_closedBall).2 ?_