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 μ
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)
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
hμU : ∀ (n : ℕ), (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n ∩ (↑I : Set (ι → ℝ))) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
x : ι → ℝ
J : Box ι
hx : x ∈ J
hJ : J ∈ π
m : ℝ≥0∞ := (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (π.filter fun (J_1 : Box ι) ↦ N (π.tag J_1) = N (π.tag J)).iUnion
⊢ x ∈ U (N (π.tag J)) ∩ (↑I : Set (ι → ℝ))

Tactic:
⟨hrU _ (hπ.1 _ hJ (Box.coe_subset_Icc hx)), π.le_of_mem' J hJ hx⟩

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate, Set.Mem, setOf, BoxIntegral.TaggedPrepartition.toPrepartition, Set.inter, And.intro, BoxIntegral.Box.coe_subset_Icc, BoxIntegral.Prepartition.le_of_mem'
-- 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_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)
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
hμU : ∀ (n : ℕ), (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n ∩ (↑I : Set (ι → ℝ))) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
x : ι → ℝ
J : Box ι
hx : x ∈ J
hJ : J ∈ π
m : ℝ≥0∞ := (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (π.filter fun (J_1 : Box ι) ↦ N (π.tag J_1) = N (π.tag J)).iUnion
⊢ x ∈ U (N (π.tag J)) ∩ (↑I : Set (ι → ℝ))

Tactic:
exact ⟨hrU _ (hπ.1 _ hJ (Box.coe_subset_Icc hx)), π.le_of_mem' J hJ hx⟩
-- 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_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 : ℕ
m : ℝ≥0∞ := (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion
⊢ m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)

Tactic:
have : m < δ n / n := by
    simp only [Measure.restrict_apply (hUo _).measurableSet] at hμU
    refine (measure_mono ?_).trans_lt (hμU _)
    simp only [Set.subset_def, TaggedPrepartition.mem_iUnion, TaggedPrepartition.mem_filter]
    rintro x ⟨J, ⟨hJ, rfl⟩, hx⟩
    exact ⟨hrU _ (hπ.1 _ hJ (Box.coe_subset_Icc hx)), π.le_of_mem' J hJ hx⟩
-- 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_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
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∞)
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_1 : π.IsPartition
n : ℕ
m : ℝ≥0∞ := (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion
this : m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
h : ∀ (m : ℝ≥0∞) (this : m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)), m.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
⊢ m.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)

Tactic:
clear_value m
-- 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_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
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∞)
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 : ℕ
m : ℝ≥0∞
this : m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ m ≠ ∞

Tactic:
ne_top_of_lt this

Premises used: ne_top_of_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_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
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∞)
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_1 : π.IsPartition
n : ℕ
m : ℝ≥0∞
this : m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
h : ∀ (m : ℝ≥0) (this : (↑m : ℝ≥0∞) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)), (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
⊢ m.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)

Tactic:
lift m to ℝ≥0 using ne_top_of_lt this

Premises used: ne_top_of_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_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
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∞)
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_1 : π.IsPartition
n : ℕ
m : ℝ≥0
this : (↑m : ℝ≥0∞) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
h : (↑m : ℝ) * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
h₁ : (↑m : ℝ) * (↑(↑n : ℝ≥0) : ℝ) ≤ (↑(δ n) : ℝ)
h₂ : (↑(m * (↑n : ℝ≥0)) : ℝ) ≤ (↑(δ n) : ℝ)
h₃ : m * (↑n : ℝ≥0) ≤ δ n
h₄ : (↑(m * (↑n : ℝ≥0)) : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
h₅ : (↑m : ℝ≥0∞) * (↑(↑n : ℝ≥0) : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
h₆ : (↑m : ℝ≥0∞) * (↑n : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
h₇ : (↑n : ℝ≥0∞) * (↑m : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
h₈ : (↑n : ℝ≥0∞) * ((↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)) ≤ (↑(δ n) : ℝ≥0∞)
h₉ h₁₀ : (↑(δ n) : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)

Tactic:
grw [ENNReal.coe_toReal, ← NNReal.coe_natCast, ← NNReal.coe_mul, NNReal.coe_le_coe, ←
    ENNReal.coe_le_coe, ENNReal.coe_mul, ENNReal.coe_natCast, mul_comm, this, ENNReal.mul_div_le]

Premises used: ENNReal.coe_toReal, ENNReal.coe_le_coe, NNReal.coe_natCast, ENNReal.mul_div_le, ENNReal.coe_mul, mul_comm, NNReal.coe_mul, ENNReal.coe_natCast, NNReal.coe_le_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 ι
y : E
f g : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f μ.toBoxAdditive.toSMul y
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
hl : l.bRiemann = false
⊢ g - f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0

Tactic:
have : g - f =ᵐ[μ.restrict I] 0 := hfg.mono fun x hx => sub_eq_zero.2 hx.symm
-- 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 ι
y : E
f g : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f μ.toBoxAdditive.toSMul y
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
hl : l.bRiemann = false
this : g - f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul y

Tactic:
simpa using hf.add (HasIntegral.of_aeEq_zero this hl)

Premises used: BoxIntegral.HasIntegral.of_aeEq_zero, BoxIntegral.HasIntegral.add
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
y : E
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ HasIntegral I l (⇑(piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0)) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
    (integral (μ.restrict (↑I : Set (ι → ℝ))) (piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0)))

Tactic:
simpa [hs] using BoxIntegral.hasIntegralIndicatorConst l hl hs I y μ

Premises used: BoxIntegral.hasIntegralIndicatorConst
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc.{u, v} (ι → ℝ) E
h :
  Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
    (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E))
hfi : HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
hgi : HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc.{u, v} (ι → ℝ) E
h :
  Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
    (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E))
hfi : HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
hgi : HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ 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
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc.{u, v} (ι → ℝ) E
h :
  Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
    (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E))
hfi : HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
hgi : HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
add :
  HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
    (integral (μ.restrict (↑I : Set (ι → ℝ))) f + integral (μ.restrict (↑I : Set (ι → ℝ))) g)
add₁ : Integrable.{v, u} (ε := E) (⇑f : (a : ι → ℝ) → E) (μ.restrict (↑I : Set (ι → ℝ)))
add₂ : Integrable.{v, u} (ε := E) (⇑g : (a : ι → ℝ) → E) (μ.restrict (↑I : Set (ι → ℝ)))
⊢ HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) (f + g))

Tactic:
rw [integral_add]

Premises used: MeasureTheory.SimpleFunc.integral_add
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc.{u, v} (ι → ℝ) E
h :
  Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
    (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E))
hfi : HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
hgi : HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
    (integral (μ.restrict (↑I : Set (ι → ℝ))) f + integral (μ.restrict (↑I : Set (ι → ℝ))) g)

Tactic:
hfi.add hgi

Premises used: BoxIntegral.HasIntegral.add
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc.{u, v} (ι → ℝ) E
h :
  Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
    (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E))
hfi : HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
hgi : HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Integrable.{v, u} (ε := E) (⇑f : (a : ι → ℝ) → E) (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
integrable_iff.2 fun _ _ => measure_lt_top _ _

Premises used: Iff.mpr, BoxIntegral.Box.toSet, MeasureTheory.measure_lt_top, MeasureTheory.Measure.restrict, MeasureTheory.SimpleFunc.integrable_iff, Set.preimage, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc.{u, v} (ι → ℝ) E
h :
  Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
    (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E))
hfi : HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
hgi : HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Integrable.{v, u} (ε := E) (⇑g : (a : ι → ℝ) → E) (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
integrable_iff.2 fun _ _ => measure_lt_top _ _

Premises used: Iff.mpr, BoxIntegral.Box.toSet, MeasureTheory.measure_lt_top, MeasureTheory.Measure.restrict, MeasureTheory.SimpleFunc.integrable_iff, Set.preimage, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc.{u, v} (ι → ℝ) E
h :
  Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
    (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E))
hfi : HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
hgi : HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
    (integral (μ.restrict (↑I : Set (ι → ℝ))) f + integral (μ.restrict (↑I : Set (ι → ℝ))) g)

Tactic:
exacts [hfi.add hgi, integrable_iff.2 fun _ _ => measure_lt_top _ _,
      integrable_iff.2 fun _ _ => measure_lt_top _ _]

Premises used: Iff.mpr, MeasureTheory.measure_lt_top, MeasureTheory.SimpleFunc.integrable_iff, Set.preimage, Singleton.singleton, DFunLike.coe, BoxIntegral.HasIntegral.add
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : SimpleFunc.{u, v} (ι → ℝ) E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
const :
  ∀ (y : E) {s : Set (ι → ℝ)} (hs : MeasurableSet s),
    HasIntegral I l (⇑(piecewise s hs (SimpleFunc.const (ι → ℝ) y) (SimpleFunc.const (ι → ℝ) 0)) : (a : ι → ℝ) → E)
      μ.toBoxAdditive.toSMul
      (integral (μ.restrict (↑I : Set (ι → ℝ)))
        (piecewise s hs (SimpleFunc.const (ι → ℝ) y) (SimpleFunc.const (ι → ℝ) 0)))
add :
  ∀ ⦃f g : SimpleFunc.{u, v} (ι → ℝ) E⦄,
    Disjoint.{u} (α := Set (ι → ℝ)) (Function.support.{u, v} (M := E) (⇑f : (a : ι → ℝ) → E))
        (Function.support.{u, v} (M := E) (⇑g : (a : ι → ℝ) → E)) →
      ∀
        (hfi :
          HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f))
        (hgi :
          HasIntegral I l (⇑g : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) g)),
        HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
          (integral (μ.restrict (↑I : Set (ι → ℝ))) (f + g))
⊢ HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)

Tactic:
induction f using MeasureTheory.SimpleFunc.induction with
  | @const y s hs =>
    simpa [hs] using BoxIntegral.hasIntegralIndicatorConst l hl hs I y μ
  | @add f g _ hfi hgi =>
    borelize E; haveI := Fact.mk (I.measure_coe_lt_top μ)
    rw [integral_add]
    exacts [hfi.add hgi, integrable_iff.2 fun _ _ => measure_lt_top _ _,
      integrable_iff.2 fun _ _ => measure_lt_top _ _]

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.const, MeasureTheory.measure_lt_top, MeasureTheory.SimpleFunc.integrable_iff, Set.preimage, Singleton.singleton, MeasureTheory.SimpleFunc.integral_add, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : SimpleFunc.{u, v} (ι → ℝ) E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
⊢ BoxIntegral.integral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul = integral (μ.restrict (↑I : Set (ι → ℝ))) f

Tactic:
(f.hasBoxIntegral μ I l hl).integral_eq

Premises used: MeasureTheory.SimpleFunc.hasBoxIntegral, BoxIntegral.HasIntegral.integral_eq
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
rcases :
  ∀ (g : (ι → ℝ) → E) (hg : StronglyMeasurable g) (hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g),
    HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)

Tactic:
rcases hf.aestronglyMeasurable with ⟨g, hg, hfg⟩

Premises used: MeasureTheory.Integrable.aestronglyMeasurable