awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 < ε
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
haveI := Fact.mk (I.measure_coe_lt_top μ)
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞))
⊢ 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

Premises used: BoxIntegral.Box.toSet, setOf, MeasureTheory.Measure.restrict, Ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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‖⌉₊
⊢ ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0

Tactic:
simp [N]
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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‖⌉₊
⊢ ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0

Tactic:
have N0 : ∀ {x}, N x = 0 ↔ f x = 0 := by simp [N]
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞)

Tactic:
(N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_

Premises used: Set.exists_isOpen_lt_of_lt, Set.preimage, Singleton.singleton
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 : ℕ
refine : (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n}) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ ∃ (U : Set (ι → ℝ)),
    N ⁻¹' {n} ⊆ U ∧
      IsOpen U ∧ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) U < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)

Tactic:
refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_

Premises used: Set.exists_isOpen_lt_of_lt, Set.preimage, Singleton.singleton
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞)
succ :
  ∀ (n : ℕ),
    (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n + 1}) <
      (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)
⊢ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n}) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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
⊢ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {0}) < (↑(δ 0) : ℝ≥0∞) / (↑0 : ℝ≥0∞)

Tactic:
simp [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne']

Premises used: Iff.mpr, LT.lt.ne', ENNReal.coe_pos, ENNReal.div_zero
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞)

Tactic:
(measure_mono_null ?_ hf).le.trans_lt ?_

Premises used: Eq.le, MeasureTheory.measure_mono_null, LE.le.trans_lt
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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}
succ₁ : 0 < (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)
⊢ (μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (N ⁻¹' {n + 1}) < (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)

Tactic:
refine (measure_mono_null ?_ hf).le.trans_lt ?_

Premises used: Eq.le, MeasureTheory.measure_mono_null, LE.le.trans_lt
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 : ℕ
⊢ N ⁻¹' {n + 1} ⊆ {x : ι → ℝ | f x ≠ 0}

Tactic:
fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)

Premises used: Iff.mpr, Set.Mem, setOf, Set.Subset, Nat.succ_ne_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 : ℕ
⊢ N ⁻¹' {n + 1} ⊆ {x : ι → ℝ | f x ≠ 0}

Tactic:
exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)

Premises used: Iff.mpr, Nat.succ_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 : ℕ
⊢ 0 < (↑(δ (n + 1)) : ℝ≥0∞) / (↑(n + 1) : ℝ≥0∞)

Tactic:
simp [(δ0 _).ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞)

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']
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞)
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 ≤ (↑ε : ℝ)
⊢ ∃ (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
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 : ι → ℝ
obtain :
  ∀ (r : ℝ) (hr₀ : 0 < r) (hr : closedBall x r ⊆ U (N x)),
    ∃ (r : (↑(Set.Ioi 0) : Type)), 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))

Premises used: Filter.HasBasis.mem_iff, IsOpen.mem_nhds, Iff.mp, Metric.nhds_basis_closedBall, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 : ℝ
hr₀ : 0 < r
hr : closedBall x r ⊆ U (N x)
⊢ ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U (N x)

Tactic:
⟨⟨r, hr₀⟩, hr⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 : ℝ
hr₀ : 0 < r
hr : closedBall x r ⊆ U (N x)
⊢ ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U (N x)

Tactic:
exact ⟨⟨r, hr₀⟩, hr⟩
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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)

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⟩
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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)
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 ≤ (↑ε : ℝ)
⊢ ∃ (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
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 ≤ (↑ε : ℝ)

Tactic:
⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ _ => ?_⟩

Premises used: And.intro, Exists.intro, BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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)
refine :
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I) (hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π),
    π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 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:
refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ _ => ?_⟩