awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx_1 :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hx :
  x ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
refine_1 :
  (prepartition n B).tag
      ((fun (x : ι → ℝ)
            (x_1 :
              x ∈
                (s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
          box n (index n x))
        x hx_1) ∈
    s
⊢ (fun (x : ι → ℝ)
            (x_1 :
              x ∈
                (s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
          box n (index n x))
        x hx_1 ∈
      (prepartition n B).boxes ∧
    (prepartition n B).tag
        ((fun (x : ι → ℝ)
              (x_1 :
                x ∈
                  (s ∩
                      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                          Set (ι → ℝ))).toFinset) ↦
            box n (index n x))
          x hx_1) ∈
      s

Tactic:
refine ⟨mem_prepartition_boxes_iff.mpr
      ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx_1 :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hx :
  x ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
refine_1 refine_1₁ : (prepartition n B).tag (box n (index n x)) ∈ s
refine_1₂ : tag n (index n x) ∈ s
refine_1₃ : x ∈ s
⊢ (prepartition n B).tag
      ((fun (x : ι → ℝ)
            (x_1 :
              x ∈
                (s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
          box n (index n x))
        x hx_1) ∈
    s

Tactic:
simp_rw [prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, hx.1]

Premises used: BoxIntegral.unitPartition.prepartition_tag, BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box, And.right, And.left, BoxIntegral.unitPartition.tag_index_eq_self_of_mem_smul_span
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
x_1 : ι → ℝ
hy :
  x_1 ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
h :
  Eq.{u_1 + 1} (α := Box ι)
    ((fun (x : ι → ℝ)
          (x_2 :
            x ∈
              (s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
        box n (index n x))
      x hx)
    ((fun (x : ι → ℝ)
          (x_2 :
            x ∈
              (s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
        box n (index n x))
      x_1 hy)
refine_2 :
  ∀
    (hx_1 :
      x ∈
        s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
    (x_2 : ι → ℝ)
    (hy :
      x_2 ∈
        (s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset)
    (hy_1 :
      x_2 ∈
        s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
    (h :
      Eq.{u_1 + 1} (α := Box ι)
        ((fun (x : ι → ℝ)
              (x_3 :
                x ∈
                  (s ∩
                      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                          Set (ι → ℝ))).toFinset) ↦
            box n (index n x))
          x hx)
        ((fun (x : ι → ℝ)
              (x_3 :
                x ∈
                  (s ∩
                      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                          Set (ι → ℝ))).toFinset) ↦
            box n (index n x))
          x_2 hy)),
    x = x_2
⊢ x = x_1

Tactic:
rw [Set.mem_toFinset] at hx hy

Premises used: Set.mem_toFinset
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx_1 :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hx :
  x ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
x_1 : ι → ℝ
hy_1 :
  x_1 ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hy :
  x_1 ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
h :
  Eq.{u_1 + 1} (α := Box ι)
    ((fun (x : ι → ℝ)
          (x_2 :
            x ∈
              (s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
        box n (index n x))
      x hx_1)
    ((fun (x : ι → ℝ)
          (x_2 :
            x ∈
              (s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
        box n (index n x))
      x_1 hy_1)
⊢ x = x_1

Tactic:
eq_of_mem_smul_span_of_index_eq_index n hx.2 hy.2 (box_injective n h)

Premises used: BoxIntegral.unitPartition.box_injective, BoxIntegral.unitPartition.eq_of_mem_smul_span_of_index_eq_index, And.right
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx_1 :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hx :
  x ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
x_1 : ι → ℝ
hy_1 :
  x_1 ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hy :
  x_1 ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
h :
  Eq.{u_1 + 1} (α := Box ι)
    ((fun (x : ι → ℝ)
          (x_2 :
            x ∈
              (s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
        box n (index n x))
      x hx_1)
    ((fun (x : ι → ℝ)
          (x_2 :
            x ∈
              (s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
        box n (index n x))
      x_1 hy_1)
⊢ x = x_1

Tactic:
exact eq_of_mem_smul_span_of_index_eq_index n hx.2 hy.2 (box_injective n h)

Premises used: BoxIntegral.unitPartition.box_injective, BoxIntegral.unitPartition.eq_of_mem_smul_span_of_index_eq_index, And.right
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
I : Box ι
hI : I ∈ {x ∈ (prepartition n B).boxes | (prepartition n B).tag x ∈ s}
⊢ I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s

Tactic:
rw [Finset.mem_filter] at hI

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
I : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ ∃ (a : ι → ℝ) (ha :
    a ∈
      (s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset),
    (fun (x : ι → ℝ)
            (x_1 :
              x ∈
                (s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
          box n (index n x))
        a ha =
      I

Tactic:
⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩

Premises used: Iff.mpr, BoxIntegral.unitPartition.box_index_tag_eq_self, BoxIntegral.TaggedPrepartition.tag, BoxIntegral.unitPartition.prepartition, And.right, And.left, And.intro, Exists.intro, Set.mem_toFinset
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
I : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
refine_3 :
  (prepartition n B).tag I ∈
    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ ∃ (a : ι → ℝ) (ha :
    a ∈
      (s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset),
    (fun (x : ι → ℝ)
            (x_1 :
              x ∈
                (s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
          box n (index n x))
        a ha =
      I

Tactic:
refine ⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
I : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
refine_3 :
  tag n (index n ((prepartition n B).tag I)) ∈
    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ (prepartition n B).tag I ∈
    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))

Tactic:
rw [← box_index_tag_eq_self n hI.1, prepartition_tag n
      (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))]

Premises used: BoxIntegral.unitPartition.prepartition_tag, BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box, BoxIntegral.unitPartition.box_index_tag_eq_self, And.right, And.left
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
I : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ tag n (index n ((prepartition n B).tag I)) ∈
    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))

Tactic:
tag_mem_smul_span _ _

Premises used: Set.Mem, BoxIntegral.unitPartition.tag_mem_smul_span
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
I : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ tag n (index n ((prepartition n B).tag I)) ∈
    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))

Tactic:
exact tag_mem_smul_span _ _

Premises used: BoxIntegral.unitPartition.tag_mem_smul_span
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
obtain :
  ∀ (B : Box ι) (hB : hasIntegralVertices B) (hs₀ : s ≤ (↑B : Set (ι → ℝ))),
    Tendsto (β := ℝ)
      (fun (n : ℕ) ↦
        (∑' (x :
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)),
            F (↑x : ι → ℝ)) /
          HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
      atTop
      (𝓝
        (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
          F x))
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x))

Tactic:
obtain ⟨B, hB, hs₀⟩ := le_hasIntegralVertices_of_isBounded hs₁

Premises used: BoxIntegral.le_hasIntegralVertices_of_isBounded
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x))

Tactic:
Metric.tendsto_atTop.mpr fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.tendsto_atTop
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
refine :
  ∀ (ε : ℝ) (hε : ε > 0),
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((∑' (x :
                (↑(s ∩
                      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                  Type u_1)),
                F (↑x : ι → ℝ)) /
              HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
            (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s)
              fun (x : ι → ℝ) ↦ F x) <
          ε
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x))

Tactic:
refine Metric.tendsto_atTop.mpr fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.tendsto_atTop
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
obtain :
  ∀ (C₀ : ℝ)
    (h₀ :
      ∀ (x : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀),
    ∃ (C : ℝ),
      ∀ (x : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
          ‖s.indicator F x‖ ≤ C
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C

Tactic:
obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn

Premises used: Continuous.continuousOn, BoxIntegral.Box.isCompact_Icc, IsCompact.exists_bound_of_continuousOn
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C

Tactic:
⟨max 0 C₀, fun x hx ↦ ?_⟩

Premises used: Max.max, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
refine :
  ∀ (x : ι → ℝ) (hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x),
    ‖s.indicator F x‖ ≤ max 0 C₀
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C

Tactic:
refine ⟨max 0 C₀, fun x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x
pos : ∀ (hs : x ∈ s), ‖F x‖ ≤ max 0 C₀
neg : ∀ (hs : x ∉ s), norm (E := ℝ) 0 ≤ max 0 C₀
⊢ ‖if x ∈ s then F x else 0‖ ≤ max 0 C₀

Tactic:
split_ifs with hs
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x
hs : x ∈ s
⊢ ‖F x‖ ≤ max 0 C₀

Tactic:
le_max_of_le_right (h₀ x hx)

Premises used: le_max_of_le_right