-- 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:
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

Tactic:
rw [Finset.mem_filter] at hI

Result:
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 ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ ∃ a,
    ∃ (ha : a ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset),
      (fun x x_1 => box n (index n x)) a ha = I

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 ι =
    ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J))

Tactic:
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]

Result:
ι : 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)

Proof state:
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))

Tactic:
rw [Set.mem_toFinset] at hx

Result:
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
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ 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_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
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (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

Tactic:
refine ⟨mem_prepartition_boxes_iff.mpr
  ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩

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
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (prepartition n B).tag ((fun x x_1 => box n (index n x)) x✝ hx✝) ∈ s

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
⊢ integralSum (s.indicator F) volume.toBoxAdditive.toSMul (prepartition n B) =
    (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι

Tactic:
unfold integralSum

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
⊢ ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J)) =
    (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι

Proof state:
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
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ 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✝))

Tactic:
rw [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.one_toReal, ENNReal.toReal_pow, ENNReal.toReal_natCast, mul_comm_div, one_mul]

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
⊢ Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Tactic:
apply Set.Finite.fintype

Result:
case h
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
⊢ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).Finite

Proof state:
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 ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ (prepartition n B).tag I ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

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

Result:
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 ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ tag n (index n ((prepartition n B).tag I)) ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))