awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
x : ι → ℝ
h_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x
⊢ r x ≤ h.convergenceR δ' C x

Tactic:
min_le_left _ _

Premises used: min_le_left
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
x : ι → ℝ
h_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x
⊢ r x ≤ h.convergenceR δ' C x

Tactic:
exact min_le_left _ _

Premises used: min_le_left
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
⊢ l.MemBaseSet J C (h.convergenceR δ' C) πJ

Tactic:
have hC₂ : l.MemBaseSet J C (h.convergenceR δ' C) πJ := by
      refine hC.mono J le_rfl le_rfl fun x _ => ?_; exact min_le_left _ _
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
hC₂ : l.MemBaseSet J C (h.convergenceR δ' C) πJ
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
⟨πJ, hp, HJi.dist_integralSum_integral_le_of_memBaseSet δ'0 hC₁ hp, hC₂⟩

Premises used: BoxIntegral.Integrable.dist_integralSum_integral_le_of_memBaseSet, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (x : ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
hC₂ : l.MemBaseSet J C (h.convergenceR δ' C) πJ
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
exact ⟨πJ, hp, HJi.dist_integralSum_integral_le_of_memBaseSet δ'0 hC₁ hp, hC₂⟩
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
⊢ ∀ J ∈ π₀,
    ∃ (πi : TaggedPrepartition J),
      πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
have : ∀ J ∈ π₀, ∃ πi : TaggedPrepartition J,
      πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧
        l.MemBaseSet J C (h.convergenceR δ' C) πi := by
    intro J hJ
    have Hle : J ≤ I := π₀.le_of_mem hJ
    have HJi : Integrable J l f vol := h.to_subbox Hle
    set r := fun x => min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
    have hJd : J.distortion ≤ C := le_trans (Finset.le_sup hJ) (le_max_left _ _)
    rcases l.exists_memBaseSet_isPartition J hJd r with ⟨πJ, hC, hp⟩
    have hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ := by
      refine hC.mono J le_rfl le_rfl fun x _ => ?_; exact min_le_right _ _
    have hC₂ : l.MemBaseSet J C (h.convergenceR δ' C) πJ := by
      refine hC.mono J le_rfl le_rfl fun x _ => ?_; exact min_le_left _ _
    exact ⟨πJ, hp, HJi.dist_integralSum_integral_le_of_memBaseSet δ'0 hC₁ hp, hC₂⟩
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
this :
  ∀ J ∈ π₀,
    ∃ (πi : TaggedPrepartition J),
      πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
choose! :
  ∀ (πi : (J : Box ι) → TaggedPrepartition J) (hπip : ∀ J ∈ π₀, (πi J).IsPartition)
    (hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ')
    (hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)),
    dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ

Tactic:
choose! πi hπip hπiδ' hπiC using this
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
⊢ l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)

Tactic:
have : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi) :=
    biUnionTagged_memBaseSet hπiC hπip fun _ => le_max_right _ _
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
⊢ π.iUnion = (π₀.biUnionTagged πi).iUnion

Tactic:
have hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion :=
    hU.trans (Prepartition.iUnion_biUnion_partition _ hπip).symm
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
⊢ dist (integralSum f vol π) (integralSum f vol (π₀.biUnionTagged πi)) ≤ ε + δ'

Tactic:
have := h.dist_integralSum_le_of_memBaseSet h0 δ'0 hπ this hU'
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this_1 : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (integralSum f vol (π₀.biUnionTagged πi)) ≤ ε + δ'
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'

Tactic:
rw [integralSum_biUnionTagged] at this

Premises used: BoxIntegral.integralSum_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this_1 : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤
    dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) +
      dist.{w} (α := F) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) (∑ J ∈ π₀.boxes, integral J l f vol)

Tactic:
dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this_1 : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) +
      dist.{w} (α := F) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) (∑ J ∈ π₀.boxes, integral J l f vol) ≤
    ε + δ' + ∑ _J ∈ π₀.boxes, δ'

Tactic:
add_le_add this (dist_sum_sum_le_of_le _ hπiδ')

Premises used: add_le_add, dist_sum_sum_le_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this_1 : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'
simp :
  ε * HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1 + δ + (↑(#π₀.boxes) : ℝ) * δ =
    HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1 * (ε + δ)
⊢ ε + δ' + ∑ _J ∈ π₀.boxes, δ' = ε + δ

Tactic:
simp [field, δ']
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this_1 : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'
⊢ ε * HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1 + δ + (↑(#π₀.boxes) : ℝ) * δ =
    HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1 * (ε + δ)

Tactic:
ring
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, Dist.dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this_1 : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : Dist.dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'
dist : ε + δ' + ∑ _J ∈ π₀.boxes, δ' = ε + δ
⊢ Dist.dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ

Tactic:
calc
    dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤
        dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) +
          dist (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) (∑ J ∈ π₀.boxes, integral J l f vol) :=
      dist_triangle _ _ _
    _ ≤ ε + δ' + ∑ _J ∈ π₀.boxes, δ' := add_le_add this (dist_sum_sum_le_of_le _ hπiδ')
    _ = ε + δ := by simp [field, δ']; ring

Premises used: dist_triangle, add_le_add, BoxIntegral.integralSum, BoxIntegral.Prepartition.boxes, dist_sum_sum_le_of_le, Dist.dist, BoxIntegral.integral, Finset.sum
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst_5 : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
⊢ dist (integralSum f vol π) (∑ J ∈ π.boxes, integral J l f vol) ≤ ε

Tactic:
h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq h0 hπ rfl

Premises used: rfl, BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Tendsto (integralSum f vol) (toFilteriUnion (l := l) I π₀) (𝓝 (∑ J ∈ π₀.boxes, integral J l f vol))

Tactic:
((l.hasBasis_toFilteriUnion I π₀).tendsto_iff nhds_basis_closedBall).2 fun ε ε0 => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
refine :
  ∀ (ε : ℝ) (ε0 : 0 < ε),
    ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
      (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
        ∀ (x : TaggedPrepartition I),
          Membership.mem (γ := Set (TaggedPrepartition I))
              {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.iUnion = π₀.iUnion} x →
            Membership.mem (γ := Set F) (closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε) (integralSum f vol x)
⊢ Tendsto (integralSum f vol) (toFilteriUnion (l := l) I π₀) (𝓝 (∑ J ∈ π₀.boxes, integral J l f vol))

Tactic:
refine ((l.hasBasis_toFilteriUnion I π₀).tendsto_iff nhds_basis_closedBall).2 fun ε ε0 => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
ε : ℝ
ε0 : 0 < ε
⊢ ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ (x : TaggedPrepartition I),
        Membership.mem (γ := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.iUnion = π₀.iUnion} x →
          Membership.mem (γ := Set F) (closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε) (integralSum f vol x)

Tactic:
⟨h.convergenceR ε, h.convergenceR_cond ε, ?_⟩

Premises used: BoxIntegral.Integrable.convergenceR, And.intro, Exists.intro, BoxIntegral.Integrable.convergenceR_cond