ι : Type u_2
I J J₁✝ J₂✝ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ : (J : Box ι) → Prepartition J
M : Type u_1
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ ↑π.boxes
J₂ : Box ι
h₂ : J₂ ∈ ↑π.boxes
hne : J₁ ≠ J₂
J' : Box ι
h₁' : J' ∈ (fun J => (πi J).boxes) J₁
h₂' : J' ∈ (fun J => (πi J).boxes) J₂
⊢ False
ι : Type u_2
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ : (J : Box ι) → Prepartition J
M : Type u_1
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ ∑ J in Finset.biUnion π.boxes fun J => (πi J).boxes, f J = ∑ J in π.boxes, ∑ J' in (πi J).boxes, f J'
refine' Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => _
no goals
ι : Type u_2
I J J₁✝ J₂✝ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ : (J : Box ι) → Prepartition J
M : Type u_1
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ ↑π.boxes
J₂ : Box ι
h₂ : J₂ ∈ ↑π.boxes
hne : J₁ ≠ J₂
J' : Box ι
h₁' : J' ∈ (fun J => (πi J).boxes) J₁
h₂' : J' ∈ (fun J => (πi J).boxes) J₂
⊢ False
exact hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))