awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] 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)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * (↑c : ℝ) * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ :
  closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ⊆
    {x_1 : Fin (n + 1) → ℝ |
      (fun (x_2 : Fin (n + 1) → ℝ) ↦
          ‖HSub.hSub (β := E) (f x_2 - f x) ((f' x : (a : Fin (n + 1) → ℝ) → E) (x_2 - x) : E)‖ ≤ ε' * ‖x_2 - x‖)
        x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J ⊆ closedBall x δ
hxJ :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ)) x
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ 0 ≤ Measure.real (m := MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ)) volume (↑J : Set (Fin (n + 1) → ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] 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)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * (↑c : ℝ) * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ :
  closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ⊆
    {x_1 : Fin (n + 1) → ℝ |
      (fun (x_2 : Fin (n + 1) → ℝ) ↦
          ‖HSub.hSub (β := E) (f x_2 - f x) ((f' x : (a : Fin (n + 1) → ℝ) → E) (x_2 - x) : E)‖ ≤ ε' * ‖x_2 - x‖)
        x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J ⊆ closedBall x δ
hxJ :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ)) x
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ LE.le (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box (Fin (n + 1))) → ℝ) J : ℝ)
    ((BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) (↑I : WithTop (Box (Fin (n + 1)))) ⋯ :
          (a : Box (Fin (n + 1))) → ℝ)
        J :
      ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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
⊢ HasIntegral.{0, u, u} (E := E) I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : 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
    (∑ i : Fin (n + 1),
      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))

Tactic:
HasIntegral.sum fun i _ => ?_

Premises used: BoxIntegral.HasIntegral.sum
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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
refine :
  ∀ (i : Fin (n + 1)),
    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))
⊢ HasIntegral.{0, u, u} (E := E) I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : 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
    (∑ i : Fin (n + 1),
      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))

Tactic:
refine HasIntegral.sum fun i _ => ?_

Premises used: BoxIntegral.HasIntegral.sum
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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
⊢ ∀ (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

Premises used: hasFDerivWithinAt_pi', continuousWithinAt_pi
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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
⊢ ∀ 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

Premises used: hasFDerivWithinAt_pi', continuousWithinAt_pi
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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
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
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
⊢ 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))

Tactic:
hasIntegral_GP_pderiv I _ _ s hs (fun x hx => Hs x hx i) (fun x hx => Hd x hx i) i

Premises used: BoxIntegral.hasIntegral_GP_pderiv
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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
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
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
⊢ 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))

Tactic:
exact hasIntegral_GP_pderiv I _ _ s hs (fun x hx => Hs x hx i) (fun x hx => Hd x hx i) i

Premises used: BoxIntegral.hasIntegral_GP_pderiv
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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)

Tactic:
HasIntegral.of_mul ‖y‖ fun ε ε0 => ?_

Premises used: Norm.norm, BoxIntegral.HasIntegral.of_mul
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 μ
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‖ * ε
⊢ HasIntegral I l (s.indicator fun (x : ι → ℝ) ↦ y) μ.toBoxAdditive.toSMul (μ.real (s ∩ (↑I : Set (ι → ℝ))) • y)

Tactic:
refine HasIntegral.of_mul ‖y‖ fun ε ε0 => ?_

Premises used: Norm.norm, BoxIntegral.HasIntegral.of_mul
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 ≤ ε

Tactic:
ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 < ε
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‖ * (↑ε : ℝ)
⊢ ∃ (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

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 < (↑ε : ℝ)
⊢ 0 < ε

Tactic:
rw [NNReal.coe_pos] at ε0

Premises used: NNReal.coe_pos
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 < ε
⊢ 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
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞)
⊢ 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
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 ⊆ s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I,
    IsClosed F ∧ (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F) < (↑ε : ℝ≥0∞)

Tactic:
(hs.inter I.measurableSet_Icc).exists_isClosed_diff_lt A (ENNReal.coe_pos.2 ε0).ne'

Premises used: Iff.mpr, BoxIntegral.Box.measurableSet_Icc, LT.lt.ne', ENNReal.coe_pos, MeasurableSet.exists_isClosed_diff_lt, MeasurableSet.inter
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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∞)
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‖ * (↑ε : ℝ)
⊢ ∃ (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'

Premises used: Iff.mpr, BoxIntegral.Box.measurableSet_Icc, BoxIntegral.Box.Icc, LT.lt.ne', ENNReal.coe_pos, MeasurableSet.exists_isClosed_diff_lt, DFunLike.coe, MeasurableSet.inter
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
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 (ι → ℝ)),
    s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ⊆ U ∧
      IsOpen U ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (U \ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) < (↑ε : ℝ≥0∞)

Tactic:
(hs.inter I.measurableSet_Icc).exists_isOpen_diff_lt A (ENNReal.coe_pos.2 ε0).ne'

Premises used: Iff.mpr, BoxIntegral.Box.measurableSet_Icc, MeasurableSet.exists_isOpen_diff_lt, LT.lt.ne', ENNReal.coe_pos, MeasurableSet.inter