awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
J : Box ι
hJ : J ∈ π.boxes ∧ π.tag J ∈ s
hJ₁ : J ∈ π.boxes
⊢ dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
      ((g : (a : Box ι) → F) J : F) ≤
    εs (π.tag J)
have hJs : π.tag J ∈ s
Tactic: obtain ⟨hJ, hJs⟩ := hJ
Cleared hypotheses: hJ
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
J : Box ι
hJ : J ∈ π.boxes
hJs : π.tag J ∈ s
⊢ dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
      ((g : (a : Box ι) → F) J : F) ≤
    εs (π.tag J)
have refine : (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall (π.tag J) (↑(δ₁ c (π.tag J) (εs (π.tag J))) : ℝ)
Tactic: refine Hδ₁ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ (hεs0 _) _ (π.le_of_mem' _ hJ) ?_
        (hπδ.2 hlH J hJ) fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
J : Box ι
hJ : J ∈ π.boxes
hJs : π.tag J ∈ s
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall (π.tag J) (↑(δ₁ c (π.tag J) (εs (π.tag J))) : ℝ)
have h : (Eq (α := ℝ → Prop) (fun (a : ℝ) ↦ 0 < a) fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) →
  δ₁ c (π.tag J) (εs (π.tag J)) = δ c (π.tag J)
Tactic: convert! hπδ.1 J hJ using 3
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
this :
  ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s},
    dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
        ((g : (a : Box ι) → F) J : F) ≤
      εs (π.tag J)
⊢ dist.{w} (α := F)
      (∑ x ∈ π.boxes with π.tag x ∈ s, (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F) (f (π.tag x)))
      (∑ x ∈ π.boxes with π.tag x ∈ s, (g : (a : Box ι) → F) x) ≤
    ε / 2
have refine_1 : ∑ b ∈ π.boxes with π.tag b ∈ s, εs (π.tag b) ≤ ε / 2
Tactic: refine (dist_sum_sum_le_of_le _ this).trans ?_
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
this :
  ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s},
    dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
        ((g : (a : Box ι) → F) J : F) ≤
      εs (π.tag J)
⊢ ∑ b ∈ π.boxes with π.tag b ∈ s, εs (π.tag b) ≤ ε / 2
have refine_1 : ∑ b ∈ Finset.image π.tag ({J ∈ π.boxes | π.tag J ∈ s}), #({a ∈ {J ∈ π.boxes | π.tag J ∈ s} | π.tag a = b}) • εs b ≤
  ε / 2
Tactic: rw [sum_comp]
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
this :
  ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s},
    dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
        ((g : (a : Box ι) → F) J : F) ≤
      εs (π.tag J)
⊢ ∑ b ∈ Finset.image π.tag ({J ∈ π.boxes | π.tag J ∈ s}), #({a ∈ {J ∈ π.boxes | π.tag J ∈ s} | π.tag a = b}) • εs b ≤
    ε / 2
have refine_1 : ∀ i ∈ Finset.image π.tag ({J ∈ π.boxes | π.tag J ∈ s}),
  #({a ∈ {J ∈ π.boxes | π.tag J ∈ s} | π.tag a = i}) • εs i ≤ HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i
Tactic: refine (sum_le_sum ?_).trans (hεs _ ?_)
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
this :
  ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s},
    dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
        ((g : (a : Box ι) → F) J : F) ≤
      εs (π.tag J)
b : ι → ℝ
⊢ #({a ∈ {J ∈ π.boxes | π.tag J ∈ s} | π.tag a = b}) • εs b ≤ HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs b
have refine_1 : #({a ∈ {J ∈ π.boxes | π.tag J ∈ s} | π.tag a = b}) • εs b ≤ HPow.hPow (α := ℕ) 2 (Fintype.card ι) • εs b
Tactic: rw [← Nat.cast_two, ← Nat.cast_pow, ← nsmul_eq_mul]
-- 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
hl : l.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c x ε) : ℝ) →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c x ε) : ℝ) →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
hlH : l.bHenstock = true
this :
  ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s},
    dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
        ((g : (a : Box ι) → F) J : F) ≤
      εs (π.tag J)
b : ι → ℝ
⊢ #({a ∈ {J ∈ π.boxes | π.tag J ∈ s} | π.tag a = b}) • εs b ≤ HPow.hPow (α := ℕ) 2 (Fintype.card ι) • εs b
have refine_1 : #({a ∈ {J ∈ π.boxes | π.tag J ∈ s} | π.tag a = b}) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card ι)
Tactic: refine nsmul_le_nsmul_left (hεs0 _).le ?_