awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
⊢ x ∈ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F

Tactic:
⟨⟨hxs, Box.coe_subset_Icc hxI⟩, fun hxF => hxt ?_⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro, BoxIntegral.Box.coe_subset_Icc
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
hbc : ∀ (hxF : x ∈ F), x ∈ t
⊢ x ∈ (s ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) \ F

Tactic:
refine ⟨⟨hxs, Box.coe_subset_Icc hxI⟩, fun hxF => hxt ?_⟩
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
hxF : x ∈ F
hbc : ∃ (i : Box ι) (_ : i ∈ π ∧ π.tag i ∈ s), x ∈ (↑i : Set (ι → ℝ))
⊢ x ∈ t

Tactic:
simp only [t, TaggedPrepartition.iUnion_def, TaggedPrepartition.mem_filter, Set.mem_iUnion]

Premises used: Set.mem_iUnion, BoxIntegral.TaggedPrepartition.mem_filter, BoxIntegral.TaggedPrepartition.iUnion_def
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
hxF : x ∈ F
hbc :
  ∀ (J : Box ι) (hJπ : J ∈ π.toPrepartition) (hxJ : x ∈ J),
    ∃ (i : Box ι) (_ : i ∈ π ∧ π.tag i ∈ s), x ∈ (↑i : Set (ι → ℝ))
⊢ ∃ (i : Box ι) (_ : i ∈ π ∧ π.tag i ∈ s), x ∈ (↑i : Set (ι → ℝ))

Tactic:
rcases hπp x hxI with ⟨J, hJπ, hxJ⟩
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
hxF : x ∈ F
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
⊢ ∃ (i : Box ι) (_ : i ∈ π ∧ π.tag i ∈ s), x ∈ (↑i : Set (ι → ℝ))

Tactic:
⟨J, ⟨hJπ, ?_⟩, hxJ⟩

Premises used: And.intro, Exists.intro
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
hxF : x ∈ F
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
hbc : π.tag J ∈ s
⊢ ∃ (i : Box ι) (_ : i ∈ π ∧ π.tag i ∈ s), x ∈ (↑i : Set (ι → ℝ))

Tactic:
refine ⟨J, ⟨hJπ, ?_⟩, hxJ⟩
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
hxF : x ∈ F
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
hbc : ∀ (hxF : π.tag J ∉ s), x ∉ F
⊢ π.tag J ∈ s

Tactic:
contrapose hxF
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
hxF : π.tag J ∉ s
⊢ x ∉ F

Tactic:
hrs'F _ ⟨π.tag_mem_Icc J, hxF⟩ ?_

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc, Set.Mem, setOf, And.intro, Not
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
hxF : π.tag J ∉ s
hbc : x ∈ closedBall (π.tag J) (↑(rs' (π.tag J)) : ℝ)
⊢ x ∉ F

Tactic:
refine hrs'F _ ⟨π.tag_mem_Icc J, hxF⟩ ?_

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc, And.intro
-- 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 (ι → ℝ)
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
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 : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := s.piecewise (β := fun (a : ι → ℝ) ↦ (↑(Set.Ioi 0) : Type)) rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun (x : ℝ≥0) ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun (x : Box ι) ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ (↑I : Set (ι → ℝ))
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ (↑I : Set (ι → ℝ))
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
hxF : π.tag J ∉ s
⊢ x ∈ closedBall (π.tag J) (↑(rs' (π.tag J)) : ℝ)

Tactic:
simpa only [r, s.piecewise_eq_of_notMem _ _ hxF] using hπ.1 J hJπ (Box.coe_subset_Icc hxJ)

Premises used: Set.piecewise_eq_of_notMem, BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul 0

Tactic:
hasIntegral_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, BoxIntegral.hasIntegral_iff
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
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 f μ.toBoxAdditive.toSMul π) 0 ≤ ε
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul 0

Tactic:
refine hasIntegral_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, BoxIntegral.hasIntegral_iff
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
ε : ℝ
ε0 : ε > 0
⊢ 0 ≤ ε

Tactic:
ε0.lt.le

Premises used: GT.gt.lt, 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
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
ε : ℝ
ε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 f μ.toBoxAdditive.toSMul π) 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 f μ.toBoxAdditive.toSMul π) 0 ≤ ε

Tactic:
lift ε to ℝ≥0 using ε0.lt.le

Premises used: GT.gt.lt, 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
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : (↑ε : ℝ) > 0
⊢ 0 < ε

Tactic:
rw [gt_iff_lt, NNReal.coe_pos] at ε0

Premises used: gt_iff_lt, 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
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hf : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] 0
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
rcases :
  ∀ (δ : ℕ → ℝ≥0) (δ0 : ∀ (i : ℕ), 0 < δ i) (c : ℝ≥0) (hδc : HasSum δ c) (hcε : c < ε),
    ∃ (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 f μ.toBoxAdditive.toSMul π) 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 f μ.toBoxAdditive.toSMul π) 0 ≤ (↑ε : ℝ)

Tactic:
rcases NNReal.exists_pos_sum_of_countable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩

Premises used: NNReal.exists_pos_sum_of_countable, LT.lt.ne', Nat