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 ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
pos :
  ∀ (h₀ : 0 < ε),
    l.RCond
      (⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
        c)
neg :
  ∀ (h₀ : ¬0 < ε),
    RCond.{u} (ι := ι) l
      ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) 1 convergenceR._proof_2)
        c)
⊢ RCond.{u} (ι := ι) l
    ((if hε : 0 < ε then
        ⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
      else fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦
        Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) 1 convergenceR._proof_2)
      c)

Tactic:
split_ifs with h₀
-- 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
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
h₀ : 0 < ε
⊢ l.RCond
    (⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
      c)

Tactic:
(hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.1 _

Premises used: Exists.choose_spec, BoxIntegral.Integrable.hasIntegral, And.left, Iff.mp, BoxIntegral.hasIntegral_iff
-- 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
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
h₀ : ¬0 < ε
⊢ RCond.{u} (ι := ι) l
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦
        Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) 1 convergenceR._proof_2)
      c)

Tactic:
fun _ x => rfl

Premises used: BoxIntegral.IntegrationParams.RCond, rfl
-- 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
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
h₀ : 0 < ε
⊢ l.RCond
    (⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
      c)

Tactic:
exacts [(hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.1 _, fun _ x => rfl]

Premises used: Exists.choose_spec, BoxIntegral.Integrable.hasIntegral, And.left, Iff.mp, BoxIntegral.hasIntegral_iff, rfl
-- 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
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
hπp : π.IsPartition
⊢ l.MemBaseSet I c
    (⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
      c)
    π

Tactic:
rw [convergenceR, dif_pos h₀] at hπ

Premises used: BoxIntegral.Integrable.convergenceR, dif_pos
-- 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
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
hπp : π.IsPartition
hπ₁ :
  l.MemBaseSet I c
    (⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
      c)
    π
⊢ π.IsPartition

Tactic:
rw [convergenceR, dif_pos h₀] at hπ

Premises used: BoxIntegral.Integrable.convergenceR, dif_pos
-- 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
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ :
  l.MemBaseSet I c
    (⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
      c)
    π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε

Tactic:
(hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.2 c _ hπ hπp

Premises used: Exists.choose_spec, BoxIntegral.Integrable.hasIntegral, And.right, Iff.mp, BoxIntegral.hasIntegral_iff
-- 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
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ :
  l.MemBaseSet I c
    (⋯.choose (p := fun (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 vol π) (integral I l f vol) ≤ ε)
      c)
    π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε

Tactic:
exact (hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.2 c _ hπ hπp

Premises used: Exists.choose_spec, BoxIntegral.Integrable.hasIntegral, And.right, Iff.mp, BoxIntegral.hasIntegral_iff
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
rcases :
  ∀ (π : Prepartition I) (hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion)
    (hπc₁ : l.bDistortion = true → π.distortion ≤ c₁) (hπc₂ : l.bDistortion = true → π.distortion ≤ c₂),
    dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂

Tactic:
rcases h₁.exists_common_compl h₂ HU with ⟨π, hπU, hπc₁, hπc₂⟩

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
⊢ dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁

Tactic:
have H₁ :
    dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁ :=
    h.dist_integralSum_integral_le_of_memBaseSet hpos₁
      (h₁.unionComplToSubordinate (fun _ _ => min_le_left _ _) hπU hπc₁)
      (isPartition_unionComplToSubordinate _ _ _ _)
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁
⊢ π.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion

Tactic:
rw [HU] at hπU
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁
hπU₁ : π.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
⊢ l.bDistortion = true → π.distortion ≤ c₁

Tactic:
rw [HU] at hπU
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁
hπU₁ : π.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
hπc₃ : l.bDistortion = true → π.distortion ≤ c₁
⊢ l.bDistortion = true → π.distortion ≤ c₂

Tactic:
rw [HU] at hπU
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁
hπU₁ : π.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
hπc₃ : l.bDistortion = true → π.distortion ≤ c₁
hπc₄ : l.bDistortion = true → π.distortion ≤ c₂
⊢ let r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x);
  dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁

Tactic:
rw [HU] at hπU
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU_1 : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU_1 r)) (integral I l f vol) ≤ ε₁
⊢ dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂

Tactic:
have H₂ :
    dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂ :=
    h.dist_integralSum_integral_le_of_memBaseSet hpos₂
      (h₂.unionComplToSubordinate (fun _ _ => min_le_right _ _) hπU hπc₂)
      (isPartition_unionComplToSubordinate _ _ _ _)
-- 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU_1 : π.iUnion = (↑I : Set (ι → ℝ)) \ π₁.iUnion
hπU : π.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (x : ι → ℝ) ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU_1 r)) (integral I l f vol) ≤ ε₁
H₂ : dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂

Tactic:
simpa [unionComplToSubordinate] using (dist_triangle_right _ _ _).trans (add_le_add H₁ H₂)

Premises used: BoxIntegral.TaggedPrepartition.unionComplToSubordinate, add_le_add, dist_triangle_right, LE.le.trans
-- 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
h : Integrable I l f vol
⊢ Tendsto (fun (π : TaggedPrepartition I × TaggedPrepartition I) ↦ (integralSum f vol π.1, integralSum f vol π.2))
    (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion}) (𝓤 F)

Tactic:
(((l.hasBasis_toFilter I).prod_self.inf_principal _).tendsto_iff
    uniformity_basis_dist_le).2 fun ε ε0 => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, BoxIntegral.IntegrationParams.hasBasis_toFilter, Filter.HasBasis.prod_self, Metric.uniformity_basis_dist_le, Filter.HasBasis.inf_principal
-- 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
h : Integrable I l f vol
refine :
  ∀ (ε : ℝ) (ε0 : 0 < ε),
    ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
      (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
        ∀
          x ∈
            SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
                {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π}
                {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π} ∩
              {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion},
          Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε}
            (integralSum f vol x.1, integralSum f vol x.2)
⊢ Tendsto (fun (π : TaggedPrepartition I × TaggedPrepartition I) ↦ (integralSum f vol π.1, integralSum f vol π.2))
    (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion}) (𝓤 F)

Tactic:
refine (((l.hasBasis_toFilter I).prod_self.inf_principal _).tendsto_iff
    uniformity_basis_dist_le).2 fun ε ε0 => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, BoxIntegral.IntegrationParams.hasBasis_toFilter, Filter.HasBasis.prod_self, Metric.uniformity_basis_dist_le, Filter.HasBasis.inf_principal
-- 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
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε
⊢ 0 < ε / 2

Tactic:
replace ε0 := half_pos ε0
-- 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
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
right :
  ∀
    x ∈
      SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
          {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
          {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} ∩
        {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion},
    Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε} (integralSum f vol x.1, integralSum f vol x.2)
⊢ ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀
        x ∈
          SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
              {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π}
              {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π} ∩
            {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion},
        Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε} (integralSum f vol x.1, integralSum f vol x.2)

Tactic:
use h.convergenceR (ε / 2), h.convergenceR_cond (ε / 2)

Premises used: BoxIntegral.Integrable.convergenceR, HDiv.hDiv, OfNat.ofNat, BoxIntegral.Integrable.convergenceR_cond
-- 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
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU :
  Membership.mem (γ := Set (TaggedPrepartition I × TaggedPrepartition I))
    {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion} (π₁, π₂)
h₁ :
  Membership.mem (γ := Set (TaggedPrepartition I))
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} (π₁, π₂).1
h₂ :
  Membership.mem (γ := Set (TaggedPrepartition I))
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} (π₁, π₂).2
right :
  Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε / 2 + ε / 2}
    (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2)
⊢ Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε}
    (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2)

Tactic:
rw [← add_halves ε]

Premises used: add_halves
-- 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
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU :
  Membership.mem (γ := Set (TaggedPrepartition I × TaggedPrepartition I))
    {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion} (π₁, π₂)
h₁ :
  Membership.mem (γ := Set (TaggedPrepartition I))
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} (π₁, π₂).1
h₂ :
  Membership.mem (γ := Set (TaggedPrepartition I))
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} (π₁, π₂).2
⊢ Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε / 2 + ε / 2}
    (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2)

Tactic:
h.dist_integralSum_le_of_memBaseSet ε0 ε0 h₁.choose_spec h₂.choose_spec hU

Premises used: Multiset.sum, Exists.choose_spec, Multiset.foldr, BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet, Set.Mem, setOf, BoxIntegral.integralSum, 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 ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU :
  Membership.mem (γ := Set (TaggedPrepartition I × TaggedPrepartition I))
    {π : TaggedPrepartition I × TaggedPrepartition I | π.1.iUnion = π.2.iUnion} (π₁, π₂)
h₁ :
  Membership.mem (γ := Set (TaggedPrepartition I))
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} (π₁, π₂).1
h₂ :
  Membership.mem (γ := Set (TaggedPrepartition I))
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} (π₁, π₂).2
⊢ Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε / 2 + ε / 2}
    (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2)

Tactic:
exact h.dist_integralSum_le_of_memBaseSet ε0 ε0 h₁.choose_spec h₂.choose_spec hU

Premises used: Exists.choose_spec, BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet