awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have rcases : ∀ (δ : ℕ → ℝ≥0) (δ0 : ∀ (i : ℕ), 0 < δ i) (c : ℝ≥0) (hδc : HasSum δ c) (hcε : c < ε),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
Tactic: rcases NNReal.exists_pos_sum_of_countable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: haveI := Fact.mk (I.measure_coe_lt_top μ)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have hf₁ : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: change μ.restrict I {x | f x ≠ 0} = 0 at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
Tactic: have N0 : ∀ {x}, N x = 0 ↔ f x = 0 := by simp [N]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
⊢ ∃ (U : Set (ι → ℝ)),
    N ⁻¹' {n} ⊆ U ∧
      IsOpen U ∧ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) U < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
have refine : (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n}) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
Tactic: refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
⊢ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n}) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
have zero : (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {0}) < (↑(δ 0) : ℝ≥0∞) / (↑0 : ℝ≥0∞)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
zero : (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {0}) < (↑(δ 0) : ℝ≥0∞) / (↑0 : ℝ≥0∞)
⊢ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n}) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
have succ : ∀ (n : ℕ),
  (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n + 1}) < (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
⊢ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n + 1}) < (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)
have succ : N ⁻¹' {n + 1} ⊆ {x : ι → ℝ | f x ≠ 0}
Tactic: refine (measure_mono_null ?_ hf).le.trans_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
succ : N ⁻¹' {n + 1} ⊆ {x : ι → ℝ | f x ≠ 0}
⊢ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n + 1}) < (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)
have succ₁ : 0 < (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)
Tactic: refine (measure_mono_null ?_ hf).le.trans_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have this₁ : ∀ (n : ℕ),
  ∃ (U : Set (ι → ℝ)),
    N ⁻¹' {n} ⊆ U ∧
      IsOpen U ∧ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) U < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
Tactic: have : ∀ n, ∃ U, N ⁻¹' {n} ⊆ U ∧ IsOpen U ∧ μ.restrict I U < δ n / n := fun n ↦ by
    refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_
    rcases n with - | n
    · simp [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne']
    · refine (measure_mono_null ?_ hf).le.trans_lt ?_
      · exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)
      · simp [(δ0 _).ne']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
this :
  ∀ (n : ℕ),
    ∃ (U : Set (ι → ℝ)),
      N ⁻¹' {n} ⊆ U ∧
        IsOpen U ∧ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) U < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have choose : ∀ (U : (n : ℕ) → Set (ι → ℝ)) (hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n) (hUo : ∀ (n : ℕ), IsOpen (U n))
  (hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
Tactic: choose U hNU hUo hμU using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
x : ι → ℝ
⊢ ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U (N x)
have obtain : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : closedBall x r ⊆ U (N x)), ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U (N x)
Tactic: obtain ⟨r, hr₀, hr⟩ := nhds_basis_closedBall.mem_iff.1 ((hUo _).mem_nhds (hNU _ rfl))
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have this₁ : ∀ (x : ι → ℝ), ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U (N x)
Tactic: have : ∀ x, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ U (N x) := fun x => by
    obtain ⟨r, hr₀, hr⟩ := nhds_basis_closedBall.mem_iff.1 ((hUo _).mem_nhds (hNU _ rfl))
    exact ⟨⟨r, hr₀⟩, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
this : ∀ (x : ι → ℝ), ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U (N x)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have choose : ∀ (r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)) (hrU : ∀ (x : ι → ℝ), closedBall x (↑(r x) : ℝ) ⊆ U (N x)),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
Tactic: choose r hrU using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrU : ∀ (x : ι → ℝ), closedBall x (↑(r x) : ℝ) ⊆ U (N x)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have refine : ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π),
  π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
Tactic: refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ _ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrU : ∀ (x : ι → ℝ), closedBall x (↑(r x) : ℝ) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
h : π.IsPartition
⊢ dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)
have rw : norm.{v} (E := E)
    (∑ y ∈ Finset.image (fun (J : Box ι) ↦ N (π.tag J)) π.boxes,
      integralSum f μ.toBoxAdditive.toSMul (π.filter fun (x : Box ι) ↦ N (π.tag x) = y)) ≤
  (↑ε : ℝ)
Tactic: rw [dist_eq_norm, sub_zero, ← integralSum_fiberwise fun J => N (π.tag J)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrU : ∀ (x : ι → ℝ), closedBall x (↑(r x) : ℝ) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
h : π.IsPartition
⊢ norm.{v} (E := E)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ N (π.tag J)) π.boxes,
        integralSum f μ.toBoxAdditive.toSMul (π.filter fun (x : Box ι) ↦ N (π.tag x) = y)) ≤
    (↑ε : ℝ)
have grw : norm.{v} (E := E)
    (∑ y ∈ Finset.image (fun (J : Box ι) ↦ N (π.tag J)) π.boxes,
      integralSum f μ.toBoxAdditive.toSMul (π.filter fun (x : Box ι) ↦ N (π.tag x) = y)) ≤
  ∑ i ∈ Finset.image (fun (J : Box ι) ↦ N (π.tag J)) π.boxes, (↑(δ i) : ℝ)
Tactic: grw [← hcε, ← sum_le_hasSum _ (fun n _ => (δ n).2) (NNReal.hasSum_coe.2 hδc)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrU : ∀ (x : ι → ℝ), closedBall x (↑(r x) : ℝ) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
h : π.IsPartition
grw :
  norm.{v} (E := E)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ N (π.tag J)) π.boxes,
        integralSum f μ.toBoxAdditive.toSMul (π.filter fun (x : Box ι) ↦ N (π.tag x) = y)) ≤
    ∑ i ∈ Finset.image (fun (J : Box ι) ↦ N (π.tag J)) π.boxes, (↑(δ i) : ℝ)
⊢ norm.{v} (E := E)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ N (π.tag J)) π.boxes,
        integralSum f μ.toBoxAdditive.toSMul (π.filter fun (x : Box ι) ↦ N (π.tag x) = y)) ≤
    (↑ε : ℝ)
have grw₁ : Finset ℕ
Tactic: grw [← hcε, ← sum_le_hasSum _ (fun n _ => (δ n).2) (NNReal.hasSum_coe.2 hδc)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
hf : Eq (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)
N : (ι → ℝ) → ℕ := fun (x : ι → ℝ) ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : (n : ℕ) → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrU : ∀ (x : ι → ℝ), closedBall x (↑(r x) : ℝ) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
h : π.IsPartition
n : ℕ
⊢ ‖integralSum f μ.toBoxAdditive.toSMul (π.filter fun (x : Box ι) ↦ N (π.tag x) = n)‖ ≤ (↑(δ n) : ℝ)
have h : norm.{v} (E := E) (∑ J ∈ (π.filter fun (x : Box ι) ↦ N (π.tag x) = n).boxes, μ.real (↑J : Set (ι → ℝ)) • f (π.tag J)) ≤
  (↑(δ n) : ℝ)
Tactic: dsimp [integralSum]