-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem integralSum_eq_tsum_div {B : Box ι} (hB : hasIntegralVertices B) (hs₀ : s ≤ B) :
    integralSum (Set.indicator s F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
      (prepartition n B) = (∑' x : ↑(s ∩ (n : ℝ)⁻¹ • L), F x) / n ^ card ι

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ Finset.filter (fun x => (prepartition n B).tag x ∈ s) (prepartition n B).boxes,
      (volume ↑x).toReal * 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 ↦ ?_)

Result:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
⊢ (fun x x_1 => box n (index n x)) x✝ hx ∈ (prepartition n B).boxes ∧
    (prepartition n B).tag ((fun x x_1 => box n (index n x)) x✝ hx) ∈ s

case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝¹ : ι → ℝ
hx : x✝¹ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
x✝ : ι → ℝ
hy : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
h : (fun x x_1 => box n (index n x)) x✝¹ hx = (fun x x_1 => box n (index n x)) x✝ hy
⊢ x✝¹ = x✝

case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
I : Box ι
hI : I ∈ Finset.filter (fun x => (prepartition n B).tag x ∈ s) (prepartition n B).boxes
⊢ ∃ a,
    ∃ (ha : a ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset),
      (fun x x_1 => box n (index n x)) a ha = I

case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
⊢ F x✝ / ↑n ^ card ι =
    (volume ↑((fun x x_1 => box n (index n x)) x✝ hx)).toReal *
      F ((prepartition n B).tag ((fun x x_1 => box n (index n x)) x✝ hx))

Proof state:
case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝¹ : ι → ℝ
hx✝ : x✝¹ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
hx : x✝¹ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
x✝ : ι → ℝ
hy✝ : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
hy : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
h : (fun x x_1 => box n (index n x)) x✝¹ hx✝ = (fun x x_1 => box n (index n x)) x✝ hy✝
⊢ x✝¹ = x✝

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

Result:
no goals