-- 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)
refine_1 :
  ∀ (x : ι → ℝ)
    (hx :
      x ∈
        (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))
          x hx ∈
        (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) ∈
        s
refine_2 :
  ∀ (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)),
    x = x_1
refine_3 :
  ∀ (I : Box ι) (hI : I ∈ {x ∈ (prepartition n B).boxes | (prepartition n B).tag x ∈ 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
refine_4 :
  ∀ (x : ι → ℝ)
    (hx :
      x ∈
        (s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset),
    F x / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι) =
      Measure.real.{u_1} (α := ι → ℝ) (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ))
          (↑((fun (x : ι → ℝ)
                    (x_1 :
                      x ∈
                        (s ∩
                            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                                Set (ι → ℝ))).toFinset) ↦
                  box n (index n x))
                x hx) :
            Set (ι → ℝ)) *
        F
          ((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))
⊢ Eq (α := ℝ)
    (∑
      i ∈
        (s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset,
      F i / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    (∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∈ s,
      Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑x : Set (ι → ℝ)) *
        F ((prepartition n B).tag x))

Tactic:
refine Finset.sum_bij (fun x _ ↦ box n (index n x)) (fun _ hx ↦ Finset.mem_filter.mpr ?_)
    (fun _ hx _ hy h ↦ ?_) (fun I hI ↦ ?_) (fun _ hx ↦ ?_)

Premises used: Iff.mpr, Finset.sum_bij, BoxIntegral.unitPartition.index, Finset.mem_filter, BoxIntegral.unitPartition.box