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
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
this : ¬Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol
neg :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    c • integral I l f vol
neg₁ :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    HSMul.hSMul (β := F) c (if h : Integrable I l f vol then Exists.choose (p := HasIntegral I l f vol) h else 0)
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have neg₂ : (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
    Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
  else 0) =
  HSMul.hSMul (β := F) c 0
Tactic: rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]
-- 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
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
this : ¬Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol
neg :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    c • integral I l f vol
neg₁ :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    HSMul.hSMul (β := F) c (if h : Integrable I l f vol then Exists.choose (p := HasIntegral I l f vol) h else 0)
neg₂ :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    HSMul.hSMul (β := F) c 0
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have neg₃ : 0 = HSMul.hSMul (β := F) c 0
Tactic: rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]
-- 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
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
this : ¬Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol
neg :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    c • integral I l f vol
neg₁ :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    HSMul.hSMul (β := F) c (if h : Integrable I l f vol then Exists.choose (p := HasIntegral I l f vol) h else 0)
neg₂ :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    HSMul.hSMul (β := F) c 0
neg₃ : 0 = HSMul.hSMul (β := F) c 0
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have neg₄ : Eq.{w + 1} (α := F) 0 0
Tactic: rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul
have pos : ∀ (hgi : Integrable I l g μ.toBoxAdditive.toSMul), 0 ≤ integral I l g μ.toBoxAdditive.toSMul
Tactic: by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
pos : ∀ (hgi : Integrable I l g μ.toBoxAdditive.toSMul), 0 ≤ integral I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul
have neg : ∀ (hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul), 0 ≤ integral I l g μ.toBoxAdditive.toSMul
Tactic: by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul
have pos : ∀ (π : TaggedPrepartition I),
  ∀ J ∈ π.boxes,
    LE.le (α := ℝ) (0 : ℝ)
      (((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
          (g (π.tag J)) :
        ℝ)
Tactic: refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul
have neg : LE.le (α := ℝ) 0
  (if h : Integrable I l g μ.toBoxAdditive.toSMul then Exists.choose (p := HasIntegral I l g μ.toBoxAdditive.toSMul) h
  else 0)
Tactic: rw [integral, dif_neg hgi]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul
neg :
  LE.le (α := ℝ) 0
    (if h : Integrable I l g μ.toBoxAdditive.toSMul then Exists.choose (p := HasIntegral I l g μ.toBoxAdditive.toSMul) h
    else 0)
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul
have neg₁ : LE.le (α := ℝ) 0 0
Tactic: rw [integral, dif_neg hgi]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
have pos : ∀ (hfi : Integrable I l f μ.toBoxAdditive.toSMul),
  ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
Tactic: by_cases hfi : Integrable.{u, v, v} I l f μ.toBoxAdditive.toSMul
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
pos :
  ∀ (hfi : Integrable I l f μ.toBoxAdditive.toSMul),
    ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
have neg : ∀ (hfi : ¬Integrable I l f μ.toBoxAdditive.toSMul),
  ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
Tactic: by_cases hfi : Integrable.{u, v, v} I l f μ.toBoxAdditive.toSMul
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
have pos : ∀ (π : TaggedPrepartition I), ‖integralSum f μ.toBoxAdditive.toSMul π‖ ≤ integralSum g μ.toBoxAdditive.toSMul π
Tactic: refine le_of_tendsto_of_tendsto' hfi.hasIntegral.norm hg.hasIntegral fun π => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
⊢ ‖integralSum f μ.toBoxAdditive.toSMul π‖ ≤ integralSum g μ.toBoxAdditive.toSMul π
have pos : ∀ J ∈ π.boxes,
  norm (E := E) ((((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (f (π.tag J)) : E) ≤
    ((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
      (g (π.tag J))
Tactic: refine norm_sum_le_of_le _ fun J _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
⊢ norm (E := E) ((((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (f (π.tag J)) : E) ≤
    ((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
      (g (π.tag J))
have pos : μ.real (↑J : Set (ι → ℝ)) * ‖f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * g (π.tag J)
Tactic: simp only [BoxAdditiveMap.toSMul_apply, norm_smul, smul_eq_mul, Real.norm_eq_abs,
      μ.toBoxAdditive_apply, abs_of_nonneg measureReal_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
⊢ μ.real (↑J : Set (ι → ℝ)) * ‖f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * g (π.tag J)
have pos : ‖f (π.tag J)‖ ≤ g (π.tag J)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : ¬Integrable I l f μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
have neg : 0 ≤ integral I l g μ.toBoxAdditive.toSMul
Tactic: rw [integral, dif_neg hfi, norm_zero]
-- 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
ε : ℝ
c : ℝ≥0
⊢ 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)
have pos : ∀ (h₀ : 0 < ε),
  l.RCond
    (sorry.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: split_ifs with h₀
-- 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
ε : ℝ
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)
⊢ 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)
have 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)
Tactic: split_ifs with h₀
-- 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
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε
have hπ₁ : l.MemBaseSet I c
  (sorry.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π
Cleared hypotheses: hπ, hπp
-- 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
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
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
have 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 π₂) ≤ ε₁ + ε₂
Tactic: rcases h₁.exists_common_compl h₂ HU with ⟨π, hπU, hπc₁, hπc₂⟩
-- 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 ι
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 π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
have H₁ : 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 _ _ _ _)
-- 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 ι
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) ≤ ε₁
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
have hπU₁ : π.iUnion = (↑I : Set (ι → ℝ)) \ π₂.iUnion
Tactic: rw [HU] at hπU
Cleared hypotheses: hπc₁, hπc₂, r, πr, H₁
-- 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 ι
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 π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
have H₂ : 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 _ _ _ _)
-- 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
⊢ 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)
have 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)
Tactic: refine (((l.hasBasis_toFilter I).prod_self.inf_principal _).tendsto_iff
    uniformity_basis_dist_le).2 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 ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε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)
have ε0₁ : 0 < ε / 2
Tactic: replace ε0 := half_pos ε0
Cleared hypotheses: ε0