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

Tactic:
rw [Set.mem_toFinset] at 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
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

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

Tactic:
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₀)

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 ℝ ι))))
⊢ ∑ 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 h
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
⊢ (s ∩ ↑(span ℤ (Set.range ⇑((Pi.basisFun ℝ ι).isUnitSMul ⋯)))).Finite

Tactic:
exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)

Result:
no goals

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
⊢ ∃ a,
    ∃ (ha : a ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset),
      (fun x x_1 => 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⟩

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

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

Tactic:
rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]

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

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 ℝ ι)))
⊢ (prepartition n B).tag ((fun x x_1 => box n (index n x)) x✝ hx✝) ∈ 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]

Result:
no goals

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

Tactic:
exact tag_mem_smul_span _ _

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
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ 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 ι

Tactic:
rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]

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

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

Tactic:
rw [Set.mem_toFinset] at hx hy

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