-- 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 (ι → ℝ))
unfold :
  ∑ J ∈ (prepartition n B).boxes,
      ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
            ℝ →L[ℝ] ℝ) :
          (a : ℝ) → ℝ)
        (s.indicator F ((prepartition n B).tag J)) =
    (∑' (x :
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
        F (↑x : ι → ℝ)) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
unfold₁ :
  ∀
    (this :
      Fintype
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
    ∑ J ∈ (prepartition n B).boxes,
        ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
              ℝ →L[ℝ] ℝ) :
            (a : ℝ) → ℝ)
          (s.indicator F ((prepartition n B).tag J)) =
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
unfold₂ :
  ∀
    (this :
      Fintype
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
    Eq (α := ℝ)
      (∑
        i ∈
          (s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset,
        F i / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
      (∑ J ∈ (prepartition n B).boxes,
        ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
              ℝ →L[ℝ] ℝ) :
            (a : ℝ) → ℝ)
          (s.indicator F ((prepartition n B).tag J)))
unfold₃ :
  ∀
    (this :
      Fintype
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
    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))
refine_1 :
  ∀
    (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),
    (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 :
  ∀
    (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)),
    x = x_1
refine_3 :
  ∀
    (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}),
    ∃ (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 :
  ∀
    (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),
    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))
refine_2₁ :
  ∀
    (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)),
    x = x_1
refine_3₁ :
  ∀
    (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}),
    ∃ (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₁ :
  ∀
    (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),
    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))
refine_3₂ :
  ∀
    (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}),
    ∃ (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₂ refine_4₃ :
  ∀
    (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),
    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))
⊢ integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B) =
    (∑' (x :
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
        F (↑x : ι → ℝ)) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)

Tactic:
classical
  unfold integralSum
  have : Fintype ↑(s ∩ (n : ℝ)⁻¹ • L) := by
    apply Set.Finite.fintype
    rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]
    exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)
  rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]
  simp_rw [Set.indicator_apply, apply_ite, BoxAdditiveMap.toSMul_apply, Measure.toBoxAdditive_apply,
    smul_eq_mul, mul_zero, Finset.sum_ite, Finset.sum_const_zero, add_zero]
  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 ↦ ?_)
  · rw [Set.mem_toFinset] at hx
    refine ⟨mem_prepartition_boxes_iff.mpr
      ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩
    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]
  · rw [Set.mem_toFinset] at hx hy
    exact eq_of_mem_smul_span_of_index_eq_index n hx.2 hy.2 (box_injective n h)
  · rw [Finset.mem_filter] at hI
    refine ⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩
    rw [← box_index_tag_eq_self n hI.1, prepartition_tag n
      (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))]
    exact tag_mem_smul_span _ _
  · rw [Set.mem_toFinset] at hx
    rw [measureReal_def, volume_box,
      prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, ENNReal.toReal_div,
      ENNReal.toReal_one, ENNReal.toReal_pow, ENNReal.toReal_natCast, mul_comm_div, one_mul]

Premises used: Iff.mpr, Set.indicator_apply, ENNReal.toReal_one, Finset.sum_bij, BoxIntegral.integralSum, apply_ite, ENNReal.toReal_natCast, eq_comm, ENNReal.toReal_pow, Finset.sum_const_zero, BoxIntegral.unitPartition.index, MulZeroClass.mul_zero, BoxIntegral.BoxAdditiveMap.toSMul_apply, Finset.sum_div, mul_comm_div, tsum_fintype, MeasureTheory.Measure.toBoxAdditive_apply, Finset.mem_filter, MeasureTheory.measureReal_def, smul_eq_mul, Set.mem_toFinset, BoxIntegral.unitPartition.volume_box, add_zero, Finset.sum_set_coe, ENNReal.toReal_div, BoxIntegral.unitPartition.box, Finset.sum_ite, one_mul, BoxIntegral.unitPartition.tag_mem_smul_span