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 μ
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) : ℝ)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h₃ : m * (↑n : ℝ≥0) ≤ δ 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]
-- 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_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
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h₄ : (↑(m * (↑n : ℝ≥0)) : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
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]
-- 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_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∞)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h₅ : (↑m : ℝ≥0∞) * (↑(↑n : ℝ≥0) : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
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]
-- 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_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∞)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h₆ : (↑m : ℝ≥0∞) * (↑n : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
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]
-- 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_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∞)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h₇ : (↑n : ℝ≥0∞) * (↑m : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
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]
-- 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_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∞)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h₈ : (↑n : ℝ≥0∞) * ((↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)) ≤ (↑(δ n) : ℝ≥0∞)
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]
-- 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_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∞)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h₉ : (↑(δ n) : ℝ≥0∞) ≤ (↑(δ n) : ℝ≥0∞)
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]
-- 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 ι
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
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul y
have this : 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
-- 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
μ : 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)
⊢ HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) (f + g))
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- 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
μ : 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
⊢ HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) (f + g))
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 (goal)
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 + g))
have add : HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
  (integral (μ.restrict (↑I : Set (ι → ℝ))) f + integral (μ.restrict (↑I : Set (ι → ℝ))) g)
Tactic: rw [integral_add]
-- 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
μ : 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)
⊢ HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) (f + g))
have add₁ : Integrable.{v, u} (ε := E) (⇑f : (a : ι → ℝ) → E) (μ.restrict (↑I : Set (ι → ℝ)))
Tactic: rw [integral_add]
-- 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
μ : 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 (ι → ℝ)))
⊢ HasIntegral I l (⇑(f + g) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) (f + g))
have add₂ : Integrable.{v, u} (ε := E) (⇑g : (a : ι → ℝ) → E) (μ.restrict (↑I : Set (ι → ℝ)))
Tactic: rw [integral_add]
-- 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
f : SimpleFunc.{u, v} (ι → ℝ) E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
⊢ HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
have const : ∀ (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: 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 _ _]
Cleared hypotheses: f
-- 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
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)))
⊢ HasIntegral I l (⇑f : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (integral (μ.restrict (↑I : Set (ι → ℝ))) f)
have 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))
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 _ _]
Cleared hypotheses: f
-- 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
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- 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
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
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)
have 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 ∂μ)
Tactic: rcases hf.aestronglyMeasurable with ⟨g, hg, hfg⟩
-- 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
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
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)
have this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
Tactic: haveI : SeparableSpace (range g ∪ {0} : Set E) := hg.separableSpace_range_union_singleton
-- 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
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)
have rw : HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ)
Tactic: rw [integral_congr_ae hfg]