awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 : ℕ
J : Box ι
hJ : J ∈ π.filter fun (J : Box ι) ↦ N (π.tag J) = n
⊢ ‖μ.real (↑J : Set (ι → ℝ)) • f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * (↑n : ℝ)
have hJ₁ : J ∈ π ∧ N (π.tag J) = n
Tactic: rw [TaggedPrepartition.mem_filter] at hJ
Cleared hypotheses: hJ
-- 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 : ℕ
J : Box ι
hJ : J ∈ π ∧ N (π.tag J) = n
⊢ ‖μ.real (↑J : Set (ι → ℝ)) • f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * (↑n : ℝ)
have rw : μ.real (↑J : Set (ι → ℝ)) * ‖f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * (↑n : ℝ)
Tactic: rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
-- 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 : ℕ
J : Box ι
hJ : J ∈ π ∧ N (π.tag J) = n
⊢ μ.real (↑J : Set (ι → ℝ)) * ‖f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * (↑n : ℝ)
have hbc : ‖f (π.tag J)‖ ≤ (↑n : ℝ)
Tactic: gcongr
-- 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_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 : ℕ
⊢ norm.{v} (E := E)
      (∑ J ∈ (π.filter fun (x : Box ι) ↦ N (π.tag x) = n).boxes, μ.real (↑J : Set (ι → ℝ)) • f (π.tag J)) ≤
    (↑(δ n) : ℝ)
have this₁ : ∀ J ∈ π.filter fun (J : Box ι) ↦ N (π.tag J) = n,
  ‖μ.real (↑J : Set (ι → ℝ)) • f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * (↑n : ℝ)
Tactic: have : ∀ J ∈ π.filter fun J => N (π.tag J) = n,
      ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real J * n := fun J hJ ↦ by
    rw [TaggedPrepartition.mem_filter] at hJ
    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
    gcongr
    exact hJ.2 ▸ Nat.le_ceil _
-- 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 : π.IsPartition
n : ℕ
this :
  ∀ J ∈ π.filter fun (J : Box ι) ↦ N (π.tag J) = n,
    ‖μ.real (↑J : Set (ι → ℝ)) • f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * (↑n : ℝ)
⊢ norm.{v} (E := E)
      (∑ J ∈ (π.filter fun (x : Box ι) ↦ N (π.tag x) = n).boxes, μ.real (↑J : Set (ι → ℝ)) • f (π.tag J)) ≤
    (↑(δ n) : ℝ)
have h : ∑ b ∈ (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).boxes, μ.real (↑b : Set (ι → ℝ)) * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
Tactic: refine (norm_sum_le_of_le _ this).trans ?_
-- 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 : ℕ
⊢ ∑ b ∈ (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).boxes, μ.real (↑b : Set (ι → ℝ)) * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h : μ.real (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
Tactic: rw [← sum_mul, ← Prepartition.measure_iUnion_toReal]
-- 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 : ℕ
m : ℝ≥0∞ := (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion
⊢ μ.real (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h : m.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
Tactic: change m.toReal * ↑n ≤ ↑(δ n)
-- 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_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∞)
have hμU₁ : ∀ (n : ℕ), (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n ∩ (↑I : Set (ι → ℝ))) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
Tactic: simp only [Measure.restrict_apply (hUo _).measurableSet] at hμU
Cleared hypotheses: hμU
-- 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)
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
hμU : ∀ (n : ℕ), (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n ∩ (↑I : Set (ι → ℝ))) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
have refine : (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion ⊆ U n ∩ (↑I : Set (ι → ℝ))
Tactic: refine (measure_mono ?_).trans_lt (hμU _)
-- 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)
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
hμU : ∀ (n : ℕ), (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U n ∩ (↑I : Set (ι → ℝ))) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion ⊆ U n ∩ (↑I : Set (ι → ℝ))
have simp : ∀ (x : ι → ℝ), (∃ (J : Box ι), (J ∈ π ∧ N (π.tag J) = n) ∧ x ∈ J) → x ∈ U n ∩ (↑I : Set (ι → ℝ))
Tactic: simp only [Set.subset_def, TaggedPrepartition.mem_iUnion, TaggedPrepartition.mem_filter]
-- 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_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.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have this₁ : 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⟩
-- 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 : π.IsPartition
n : ℕ
m : ℝ≥0∞ := (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (π.filter fun (J : Box ι) ↦ N (π.tag J) = n).iUnion
this : m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ m.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h : ∀ (m : ℝ≥0∞) (this : m < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)), m.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
Tactic: clear_value m
Cleared hypotheses: m, 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_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.toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h : ∀ (m : ℝ≥0) (this : (↑m : ℝ≥0∞) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)), (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
Tactic: lift m to ℝ≥0 using ne_top_of_lt this
Cleared hypotheses: m, 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_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 : ℝ≥0∞) < (↑(δ n) : ℝ≥0∞) / (↑n : ℝ≥0∞)
⊢ (↑m : ℝ≥0∞).toReal * (↑n : ℝ) ≤ (↑(δ n) : ℝ)
have h : (↑m : ℝ) * (↑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]
-- 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) : ℝ)
⊢ (↑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) : ℝ)
⊢ (↑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]