awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use h.convergenceR (ε / 2), h.convergenceR_cond (ε / 2)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 ≤ ε}
    (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2)
have right : Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε / 2 + ε / 2}
  (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2)
Tactic: rw [← add_halves ε]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 π₀))
have refine : Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀) ×ˢ
    Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀) ≤
  𝓤 F
Tactic: refine ⟨inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 (integralSum f vol) (toFilteriUnion (l := l) I π₀) ×ˢ
      Filter.map (integralSum f vol) (toFilteriUnion (l := l) I π₀) ≤
    𝓤 F
have 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
Tactic: rw [prod_map_map_eq, ← toFilter_inf_iUnion_eq, ← prod_inf_prod, prod_principal_principal]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
have refine : ∀ (y : F) (hy : Tendsto (integralSum f vol) (toFilteriUnion (l := l) I (Prepartition.single I J hJ)) (𝓝 y)),
  HasIntegral J l f vol y
Tactic: refine (cauchy_map_iff_exists_tendsto.1
    (h.cauchy_map_integralSum_toFilteriUnion (.single I J hJ))).imp fun y hy ↦ ⟨?_, hy⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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) ≤ ε
have refine : ∀ (δ : ℝ) (δ0 : 0 < δ), dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
Tactic: refine le_of_forall_pos_le_add fun δ δ0 => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
have H0 : 0 < HAdd.hAdd (α := ℝ) (↑(#π₀.boxes) : ℝ) 1
Tactic: have H0 : 0 < (#π₀.boxes + 1 : ℝ) := Nat.cast_add_one_pos _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
have δ'0 : 0 < δ'
Tactic: have δ'0 : 0 < δ' := div_pos δ0 H0
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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 ∈ π₀
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
have Hle : J ≤ I
Tactic: have Hle : J ≤ I := π₀.le_of_mem hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
have HJi : Integrable J l f vol
Tactic: have HJi : Integrable J l f vol := h.to_subbox Hle
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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)
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
have hJd : J.distortion ≤ C
Tactic: have hJd : J.distortion ≤ C := le_trans (Finset.le_sup hJ) (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
have 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
Tactic: rcases l.exists_memBaseSet_isPartition J hJd r with ⟨πJ, hC, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
have refine : ∀ (x : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
    r x ≤ HJi.convergenceR δ' C x
Tactic: refine hC.mono J le_rfl le_rfl fun x _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
have hC₁ : 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 _ _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
have refine : ∀ (x : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
    r x ≤ h.convergenceR δ' C x
Tactic: refine hC.mono J le_rfl le_rfl fun x _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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
⊢ ∃ (πi : TaggedPrepartition J),
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
have hC₂ : 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 _ _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
have 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
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₂⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
have 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) ≤ ε + δ
Tactic: choose! πi hπip hπiδ' hπiC using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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)
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
have this : 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 _ _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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)
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
have hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
Tactic: have hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion :=
    hU.trans (Prepartition.iUnion_biUnion_partition _ hπip).symm
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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 π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
have this₁ : dist (integralSum f vol π) (integralSum f vol (π₀.biUnionTagged πi)) ≤ ε + δ'
Tactic: have := h.dist_integralSum_le_of_memBaseSet h0 δ'0 hπ this hU'