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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
⊢ Eq.{w + 1} (α := F)
    (∑ J' ∈ (πi J).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((π.biUnionPrepartition πi).tag J')) :
      F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)

Tactic:
calc
    (∑ J' ∈ (πi J).boxes, vol J' (f (π.tag <| π.toPrepartition.biUnionIndex πi J'))) =
        ∑ J' ∈ (πi J).boxes, vol J' (f (π.tag J)) :=
      sum_congr rfl fun J' hJ' => by rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']
    _ = vol J (f (π.tag J)) :=
      (vol.map ⟨⟨fun g : E →L[ℝ] F => g (f (π.tag J)), rfl⟩, fun _ _ => rfl⟩).sum_partition_boxes
        le_top (hπi J hJ)

Premises used: BoxIntegral.BoxAdditiveMap.map, BoxIntegral.Prepartition.biUnionIndex, AddMonoidHom.mk, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.TaggedPrepartition.tag, BoxIntegral.Prepartition.boxes, ZeroHom.mk, BoxIntegral.BoxAdditiveMap.sum_partition_boxes, le_top, DFunLike.coe, Finset.sum_congr, Finset.sum, 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
π' : Prepartition I
h : π'.IsPartition
⊢ integralSum f vol (π.infPrepartition π') = integralSum f vol π

Tactic:
integralSum_biUnion_partition f vol π _ fun _J hJ => h.restrict (Prepartition.le_of_mem _ hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, BoxIntegral.TaggedPrepartition.infPrepartition, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.integralSum_biUnion_partition, BoxIntegral.Prepartition.IsPartition.restrict
-- 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 ι
α : Type u_1
g : Box ι → α
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ ∑ y ∈ Finset.image g π.boxes, integralSum f vol (π.filter fun (x : Box ι) ↦ g x = y) = integralSum f vol π

Tactic:
π.sum_fiberwise g fun J => vol J (f <| π.tag J)

Premises used: BoxIntegral.Prepartition.sum_fiberwise, BoxIntegral.integralSum, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.TaggedPrepartition.tag, DFunLike.coe
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
rw :
  HSub.hSub (α := F)
      (∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
          (f ((π₁.infPrepartition π₂.toPrepartition).tag J)))
      (∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
          (f ((π₂.infPrepartition π₁.toPrepartition).tag J))) =
    HSub.hSub (α := F)
      (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F)
          (f ((π₁.infPrepartition π₂.toPrepartition).tag x)))
      (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F)
          (f ((π₂.infPrepartition π₁.toPrepartition).tag x)))
⊢ integralSum f vol π₁ - integralSum f vol π₂ =
    ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      HSub.hSub (α := F) (β := F)
        ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
            (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) :
          F)
        ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
            (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) :
          F)

Tactic:
rw [← integralSum_inf_partition f vol π₁ h₂, ← integralSum_inf_partition f vol π₂ h₁,
    integralSum, integralSum, Finset.sum_sub_distrib]

Premises used: BoxIntegral.integralSum_inf_partition, BoxIntegral.integralSum, Finset.sum_sub_distrib
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ HSub.hSub (α := F)
      (∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
          (f ((π₁.infPrepartition π₂.toPrepartition).tag J)))
      (∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
          (f ((π₂.infPrepartition π₁.toPrepartition).tag J))) =
    HSub.hSub (α := F)
      (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F)
          (f ((π₁.infPrepartition π₂.toPrepartition).tag x)))
      (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F)
          (f ((π₂.infPrepartition π₁.toPrepartition).tag x)))

Tactic:
simp only [infPrepartition_toPrepartition, inf_comm]

Premises used: inf_comm, BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂

Tactic:
(Prepartition.sum_disj_union_boxes h _).trans
      (congr_arg₂ (· + ·) (sum_congr rfl fun J hJ => ?_) (sum_congr rfl fun J hJ => ?_))

Premises used: BoxIntegral.integralSum, BoxIntegral.Prepartition.sum_disj_union_boxes, HAdd.hAdd, Finset.sum_congr, rfl, Eq.trans, congr_arg₂
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.boxes),
    Eq.{w + 1} (α := F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
refine_2 :
  ∀ (J : Box ι) (hJ : J ∈ π₂.boxes),
    Eq.{w + 1} (α := F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)
⊢ integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂

Tactic:
refine (Prepartition.sum_disj_union_boxes h _).trans
      (congr_arg₂ (· + ·) (sum_congr rfl fun J hJ => ?_) (sum_congr rfl fun J hJ => ?_))

Premises used: BoxIntegral.Prepartition.sum_disj_union_boxes, HAdd.hAdd, Finset.sum_congr, rfl, Eq.trans, congr_arg₂
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₁.boxes
refine_1 refine_1₁ :
  Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)

Tactic:
rw [disjUnion_tag_of_mem_left _ hJ]

Premises used: BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
refine_2 refine_2₁ :
  Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

Premises used: BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_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 ι
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ integralSum (f + g) vol π = integralSum f vol π + integralSum g vol π

Tactic:
simp only [integralSum, Pi.add_apply, (vol _).map_add, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, BoxIntegral.integralSum, Pi.add_apply, ContinuousLinearMap.map_add, DFunLike.coe
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ integralSum (-f) vol π = -integralSum f vol π

Tactic:
simp only [integralSum, Pi.neg_apply, (vol _).map_neg, Finset.sum_neg_distrib]

Premises used: BoxIntegral.integralSum, Finset.sum_neg_distrib, Pi.neg_apply, ContinuousLinearMap.map_neg, DFunLike.coe
-- 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 ι
c : ℝ
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ integralSum (c • f) vol π = c • integralSum f vol π

Tactic:
simp only [integralSum, Finset.smul_sum, Pi.smul_apply, map_smul]

Premises used: BoxIntegral.integralSum, Finset.smul_sum, map_smul, Pi.smul_apply
-- 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
y : F
h : HasIntegral I l f vol y
⊢ Tendsto (integralSum f vol) (toFilteriUnion (l := l) I ⊤) (𝓝 y)

Tactic:
h

Premises used: BoxIntegral.HasIntegral
-- 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
y : F
⊢ (∀ (ib : ℝ),
      0 < ib →
        ∃ (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) π ∧ π.IsPartition} x →
                integralSum f vol x ∈ closedBall y ib) ↔
    ∀ ε > 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 vol π) y ≤ ε

Tactic:
simp [@forall_comm ℝ≥0 (TaggedPrepartition I)]

Premises used: forall_comm
-- 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
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    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 vol π) y ≤ a * ε
⊢ HasIntegral I l f vol y

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

Premises used: Iff.mpr, 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
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    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 vol π) y ≤ a * ε
refine :
  ∀ (ε : ℝ) (hε : ε > 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 vol π) y ≤ ε
⊢ HasIntegral I l f vol y

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

Premises used: Iff.mpr, 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
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    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 vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
rcases :
  ∀ (ε' : ℝ) (hε' : 0 < ε') (ha : a * ε' < ε),
    ∃ (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 π) 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 f vol π) y ≤ ε

Tactic:
rcases exists_pos_mul_lt hε a with ⟨ε', hε', ha⟩

Premises used: exists_pos_mul_lt
-- 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
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    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 vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
ε' : ℝ
hε' : 0 < ε'
ha : a * ε' < ε
rcases :
  ∀ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) (hr : ∀ (c : ℝ≥0), l.RCond (r c))
    (H :
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε'),
    ∃ (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 π) 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 f vol π) y ≤ ε

Tactic:
rcases h ε' hε' with ⟨r, hr, 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
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    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 vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
ε' : ℝ
hε' : 0 < ε'
ha : a * ε' < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr : ∀ (c : ℝ≥0), l.RCond (r c)
H :
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
    l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε'
⊢ ∃ (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 π) y ≤ ε

Tactic:
⟨r, hr, fun c π hπ hπp => (H c π hπ hπp).trans ha.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro, 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
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    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 vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
ε' : ℝ
hε' : 0 < ε'
ha : a * ε' < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr : ∀ (c : ℝ≥0), l.RCond (r c)
H :
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
    l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε'
⊢ ∃ (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 π) y ≤ ε

Tactic:
exact ⟨r, hr, fun c π hπ hπp => (H c π hπ hπp).trans ha.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 ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
⊢ Integrable I l f vol ↔ Cauchy (Filter.map (integralSum f vol) (toFilteriUnion (l := l) I ⊤))

Tactic:
cauchy_map_iff_exists_tendsto.symm

Premises used: BoxIntegral.Integrable, cauchy_map_iff_exists_tendsto, Iff.symm, BoxIntegral.HasIntegral
-- 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
rw :
  (∀ (ib : ℝ),
      0 < ib →
        ∃ (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) π ∧ π.IsPartition}
                  {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.IsPartition},
              Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ib}
                (integralSum f vol x.1, integralSum f vol x.2)) ↔
    ∀ ε > 0,
      ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
            l.MemBaseSet I c₁ (r c₁) π₁ →
              π₁.IsPartition →
                l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε
⊢ Integrable I l f vol ↔
    ∀ ε > 0,
      ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
            l.MemBaseSet I c₁ (r c₁) π₁ →
              π₁.IsPartition →
                l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε

Tactic:
rw [integrable_iff_cauchy, cauchy_map_iff',
    (l.hasBasis_toFilteriUnion_top _).prod_self.tendsto_iff uniformity_basis_dist_le]

Premises used: Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top, Metric.uniformity_basis_dist_le, BoxIntegral.integrable_iff_cauchy, cauchy_map_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
inst_5 : CompleteSpace F
⊢ (∀ (ib : ℝ),
      0 < ib →
        ∃ (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) π ∧ π.IsPartition}
                  {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.IsPartition},
              Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ib}
                (integralSum f vol x.1, integralSum f vol x.2)) ↔
    ∀ ε > 0,
      ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
            l.MemBaseSet I c₁ (r c₁) π₁ →
              π₁.IsPartition →
                l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε

Tactic:
forall₂_congr fun ε _ => exists_congr fun r => ?_

Premises used: exists_congr, forall₂_congr