awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ HasIntegral I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
    BoxAdditiveMap.volume
    (HSub.hSub (α := E)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
        BoxAdditiveMap.volume)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
        BoxAdditiveMap.volume))
have Hd₁ : ∀ (x : Fin (n + 1) → ℝ),
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
    ∀ (i : Fin (n + 1)),
      HasFDerivWithinAt (fun (x : Fin (n + 1) → ℝ) ↦ f x i)
        (ContinuousLinearMap.proj (φ := fun (i : Fin (n + 1)) ↦ E) i ∘SL f' x)
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Tactic: simp only [hasFDerivWithinAt_pi', continuousWithinAt_pi] at Hd Hs
Cleared hypotheses: Hs, Hd
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
Hd₁ :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      ∀ (i : Fin (n + 1)),
        HasFDerivWithinAt (fun (x : Fin (n + 1) → ℝ) ↦ f x i)
          (ContinuousLinearMap.proj (φ := fun (i : Fin (n + 1)) ↦ E) i ∘SL f' x)
          ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
⊢ HasIntegral I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
    BoxAdditiveMap.volume
    (HSub.hSub (α := E)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
        BoxAdditiveMap.volume)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
        BoxAdditiveMap.volume))
have Hs₁ : ∀ x ∈ s,
  ∀ (i : Fin (n + 1)),
    ContinuousWithinAt.{0, u} (Y := E) (fun (y : Fin (n + 1) → ℝ) ↦ f y i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Tactic: simp only [hasFDerivWithinAt_pi', continuousWithinAt_pi] at Hd Hs
Cleared hypotheses: Hs, Hd
-- 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
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
⊢ HasIntegral I l (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y)
have refine : ∀ (ε : ℝ) (ε0 : 0 < ε),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * ε
Tactic: refine HasIntegral.of_mul ‖y‖ fun ε ε0 => ?_
-- 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
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ
ε0 : 0 < ε
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * ε
have lift : ∀ (ε : ℝ≥0) (ε0 : 0 < (↑ε : ℝ)),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
Tactic: lift ε to ℝ≥0 using ε0.le
Cleared hypotheses: ε, ε0
-- 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
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have ε0₁ : 0 < ε
Tactic: rw [NNReal.coe_pos] at ε0
Cleared hypotheses: ε0
-- 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
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have A : μ (s ∩ Box.Icc I) ≠ ∞ :=
    ((measure_mono Set.inter_subset_right).trans_lt (I.measure_Icc_lt_top μ)).ne
-- 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
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have B : μ (s ∩ I) ≠ ∞ :=
    ((measure_mono Set.inter_subset_right).trans_lt (I.measure_coe_lt_top μ)).ne
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have obtain : ∀ (F : Set (ι → ℝ)) (hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) (hFc : IsClosed F)
  (hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
Tactic: obtain ⟨F, hFs, hFc, hμF⟩ : ∃ F, F ⊆ s ∩ Box.Icc I ∧ IsClosed F ∧ μ ((s ∩ Box.Icc I) \ F) < ε :=
    (hs.inter I.measurableSet_Icc).exists_isClosed_diff_lt A (ENNReal.coe_pos.2 ε0).ne'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have obtain : ∀ (U : Set (ι → ℝ)) (hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U) (hUo : IsOpen U)
  (hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
Tactic: obtain ⟨U, hsU, hUo, hUt, hμU⟩ :
      ∃ U, s ∩ Box.Icc I ⊆ U ∧ IsOpen U ∧ μ U < ∞ ∧ μ (U \ (s ∩ Box.Icc I)) < ε :=
    (hs.inter I.measurableSet_Icc).exists_isOpen_diff_lt A (ENNReal.coe_pos.2 ε0).ne'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
x : ι → ℝ
hx : x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
⊢ ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U
have rcases : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : closedBall x r ⊆ U), ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U
Tactic: rcases nhds_basis_closedBall.mem_iff.1 (hUo.mem_nhds <| hsU hx) with ⟨r, hr₀, hr⟩
-- 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
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have this : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U
Tactic: have : ∀ x ∈ s ∩ Box.Icc I, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ U := fun x hx => by
    rcases nhds_basis_closedBall.mem_iff.1 (hUo.mem_nhds <| hsU hx) with ⟨r, hr₀, hr⟩
    exact ⟨⟨r, hr₀⟩, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
this : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ U
⊢ ∃ (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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have choose! : ∀ (rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type))
  (hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U),
  ∃ (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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
Tactic: choose! rs hrsU using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x
⊢ ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ Fᶜ
have obtain : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : closedBall x r ⊆ Fᶜ), ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ Fᶜ
Tactic: obtain ⟨r, hr₀, hr⟩ :=
      nhds_basis_closedBall.mem_iff.1 (hFc.isOpen_compl.mem_nhds fun hx' => hx.2 (hFs hx').1)
-- 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
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
⊢ ∃ (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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have this : ∀ (x : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
    ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ Fᶜ
Tactic: have : ∀ x ∈ Box.Icc I \ s, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ Fᶜ := fun x hx => by
    obtain ⟨r, hr₀, hr⟩ :=
      nhds_basis_closedBall.mem_iff.1 (hFc.isOpen_compl.mem_nhds fun hx' => hx.2 (hFs hx').1)
    exact ⟨⟨r, hr₀⟩, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
hFc : IsClosed F
hμF : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)
U : Set (ι → ℝ)
hsU : s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U
hUo : IsOpen U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)
rs : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type)
hrsU : ∀ x ∈ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I, closedBall x (↑(rs x) : ℝ) ⊆ U
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∃ (r : (↑(Set.Ioi 0) : Type)), closedBall x (↑r : ℝ) ⊆ Fᶜ
⊢ ∃ (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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
have choose! : ∀ (rs' : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type))
  (hrs'F :
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
        closedBall x (↑(rs' x) : ℝ) ⊆ Fᶜ),
  ∃ (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 (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul π)
                (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y) ≤
              ‖y‖ * (↑ε : ℝ)
Tactic: choose! rs' hrs'F using this
Cleared hypotheses: this