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
π₀ : Prepartition I
⊢ Cauchy (Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀))

Tactic:
⟨inferInstance, ?_⟩

Premises used: Cauchy, inferInstance, And.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 ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
refine :
  Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀) ×ˢ
      Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀) ≤
    𝓤 F
⊢ Cauchy (Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀))

Tactic:
refine ⟨inferInstance, ?_⟩
-- 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
π₀ : Prepartition I
rw :
  Filter.map (fun (p : TaggedPrepartition I × TaggedPrepartition I) ↦ (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓
        𝓟
          (SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | π.iUnion = π₀.iUnion} {π : TaggedPrepartition I | π.iUnion = π₀.iUnion})) ≤
    𝓤 F
⊢ Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀) ×ˢ
      Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀) ≤
    𝓤 F

Tactic:
rw [prod_map_map_eq, ← toFilter_inf_iUnion_eq, ← prod_inf_prod, prod_principal_principal]

Premises used: BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq, Filter.prod_inf_prod, Filter.prod_principal_principal, Filter.prod_map_map_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
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (fun (p : TaggedPrepartition I × TaggedPrepartition I) ↦ (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓
        𝓟
          (SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | π.iUnion = π₀.iUnion} {π : TaggedPrepartition I | π.iUnion = π₀.iUnion})) ≤
    𝓤 F

Tactic:
h.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity.mono_left
    (inf_le_inf_left _ <| principal_mono.2 fun π h => h.1.trans h.2.symm)

Premises used: Iff.mpr, Filter.principal_mono, inf_le_inf_left, And.right, And.left, Filter.Tendsto, BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity, Filter.Tendsto.mono_left, Eq.symm, Eq.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
π₀ : Prepartition I
⊢ Filter.map (fun (p : TaggedPrepartition I × TaggedPrepartition I) ↦ (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓
        𝓟
          (SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | π.iUnion = π₀.iUnion} {π : TaggedPrepartition I | π.iUnion = π₀.iUnion})) ≤
    𝓤 F

Tactic:
exact h.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity.mono_left
    (inf_le_inf_left _ <| principal_mono.2 fun π h => h.1.trans h.2.symm)

Premises used: Iff.mpr, Filter.principal_mono, inf_le_inf_left, BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity, Filter.Tendsto.mono_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 J : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
⊢ ∃ (y : F),
    HasIntegral J l f vol y ∧ Tendsto (integralSum f vol) (toFilteriUnion (l := l) I (Prepartition.single I J hJ)) (𝓝 y)

Tactic:
(cauchy_map_iff_exists_tendsto.1
    (h.cauchy_map_integralSum_toFilteriUnion (.single I J hJ))).imp fun y hy ↦ ⟨?_, hy⟩

Premises used: cauchy_map_iff_exists_tendsto, BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion, BoxIntegral.Prepartition.single, Exists.imp, And.intro, Iff.mp
-- 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 J : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
refine :
  ∀ (y : F) (hy : Tendsto (integralSum f vol) (toFilteriUnion (l := l) I (Prepartition.single I J hJ)) (𝓝 y)),
    HasIntegral J l f vol y
⊢ ∃ (y : F),
    HasIntegral J l f vol y ∧ Tendsto (integralSum f vol) (toFilteriUnion (l := l) I (Prepartition.single I J hJ)) (𝓝 y)

Tactic:
refine (cauchy_map_iff_exists_tendsto.1
    (h.cauchy_map_integralSum_toFilteriUnion (.single I J hJ))).imp fun y hy ↦ ⟨?_, hy⟩

Premises used: cauchy_map_iff_exists_tendsto, BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion, BoxIntegral.Prepartition.single, Exists.imp, Iff.mp
-- 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 J : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
y : F
hy : Tendsto (integralSum f vol) (toFilteriUnion (l := l) I (Prepartition.single I J hJ)) (𝓝 y)
⊢ Tendsto
    (comp (β := TaggedPrepartition I) (integralSum f vol)
      (⇑(embedBox J I hJ) : (a : TaggedPrepartition J) → TaggedPrepartition I))
    (toFilteriUnion (l := l) J ⊤) (𝓝 y)

Tactic:
hy.comp
      (l.tendsto_embedBox_toFilteriUnion_top hJ)

Premises used: BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top, Filter.Tendsto.comp
-- 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 J : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
y : F
hy : Tendsto (integralSum f vol) (toFilteriUnion (l := l) I (Prepartition.single I J hJ)) (𝓝 y)
⊢ HasIntegral J l f vol y

Tactic:
convert!
    hy.comp
      (l.tendsto_embedBox_toFilteriUnion_top hJ)

Premises used: BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top, Filter.Tendsto.comp
-- 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 J : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
⊢ Integrable J l f vol

Tactic:
(h.to_subbox_aux hJ).imp fun _ => And.left

Premises used: BoxIntegral.Integrable, BoxIntegral.Integrable.to_subbox_aux, Exists.imp, And.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 J : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
h : Integrable I l f vol
hJ : J ≤ I
⊢ Tendsto (integralSum f vol) (toFilteriUnion (l := l) I (Prepartition.single I J hJ)) (𝓝 (integral J l f vol))

Tactic:
let ⟨_y, h₁, h₂⟩ := h.to_subbox_aux hJ
  h₁.integral_eq.symm ▸ h₂

Premises used: BoxIntegral.IntegrationParams.toFilteriUnion, BoxIntegral.Integrable.to_subbox_aux, BoxIntegral.integralSum, nhds, Eq.rec, BoxIntegral.Prepartition.single, Filter.Tendsto, _private.0.BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single.match_1, Eq.symm, BoxIntegral.integral, BoxIntegral.HasIntegral.integral_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 ι
π : 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
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε

Tactic:
le_of_forall_pos_le_add fun δ δ0 => ?_

Premises used: le_of_forall_pos_le_add
-- 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
refine : ∀ (δ : ℝ) (δ0 : 0 < δ), dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε

Tactic:
refine le_of_forall_pos_le_add fun δ δ0 => ?_

Premises used: le_of_forall_pos_le_add
-- 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
⊢ 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1

Tactic:
have H0 : 0 < (#π₀.boxes + 1 : ℝ) := Nat.cast_add_one_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
ε : ℝ
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 < δ'

Tactic:
have δ'0 : 0 < δ' := div_pos δ0 H0
-- 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 ∈ π₀
⊢ J ≤ I

Tactic:
have Hle : J ≤ I := π₀.le_of_mem hJ
-- 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
⊢ Integrable J l f vol

Tactic:
have HJi : Integrable J l f vol := h.to_subbox Hle
-- 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)
⊢ J.distortion ≤ C

Tactic:
have hJd : J.distortion ≤ C := le_trans (Finset.le_sup hJ) (le_max_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
rcases :
  ∀ (πJ : TaggedPrepartition J) (hC : l.MemBaseSet J C r πJ) (hp : πJ.IsPartition),
    ∃ (πi : TaggedPrepartition J),
      πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
rcases l.exists_memBaseSet_isPartition J hJd r with ⟨πJ, hC, hp⟩

Premises used: BoxIntegral.IntegrationParams.exists_memBaseSet_isPartition
-- 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
⊢ l.MemBaseSet J C (HJi.convergenceR δ' C) πJ

Tactic:
hC.mono J le_rfl le_rfl fun x _ => ?_

Premises used: le_rfl, BoxIntegral.IntegrationParams.MemBaseSet.mono
-- 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
refine :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
      r x ≤ HJi.convergenceR δ' C x
⊢ l.MemBaseSet J C (HJi.convergenceR δ' C) πJ

Tactic:
refine hC.mono J le_rfl le_rfl fun x _ => ?_

Premises used: le_rfl, BoxIntegral.IntegrationParams.MemBaseSet.mono
-- 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
x : ι → ℝ
h_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x
⊢ r x ≤ HJi.convergenceR δ' C x

Tactic:
min_le_right _ _

Premises used: min_le_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
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
x : ι → ℝ
h_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x
⊢ r x ≤ HJi.convergenceR δ' C x

Tactic:
exact min_le_right _ _

Premises used: min_le_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
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
⊢ l.MemBaseSet J C (HJi.convergenceR δ' C) πJ

Tactic:
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 _ _
-- 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:
hC.mono J le_rfl le_rfl fun x _ => ?_

Premises used: le_rfl, BoxIntegral.IntegrationParams.MemBaseSet.mono
-- 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
refine :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
      r x ≤ h.convergenceR δ' C x
⊢ l.MemBaseSet J C (h.convergenceR δ' C) πJ

Tactic:
refine hC.mono J le_rfl le_rfl fun x _ => ?_

Premises used: le_rfl, BoxIntegral.IntegrationParams.MemBaseSet.mono