ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : IsPartition π₁
h₂ : IsPartition π₂
⊢ ∑ J in (infPrepartition π₁ π₂.toPrepartition).toPrepartition.boxes,
        ↑(↑vol J) (f (tag (infPrepartition π₁ π₂.toPrepartition) J)) -
      ∑ J in (infPrepartition π₂ π₁.toPrepartition).toPrepartition.boxes,
        ↑(↑vol J) (f (tag (infPrepartition π₂ π₁.toPrepartition) J)) =
    ∑ x in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ↑(↑vol x) (f (tag (infPrepartition π₁ π₂.toPrepartition) x)) -
      ∑ x in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ↑(↑vol x) (f (tag (infPrepartition π₂ π₁.toPrepartition) x))
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : IsPartition π₁
h₂ : IsPartition π₂
⊢ integralSum f vol π₁ - integralSum f vol π₂ =
    ∑ J in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      (↑(↑vol J) (f (tag (infPrepartition π₁ π₂.toPrepartition) J)) -
        ↑(↑vol J) (f (tag (infPrepartition π₂ π₁.toPrepartition) J)))
rw [← integralSum_inf_partition f vol π₁ h₂, ← integralSum_inf_partition f vol π₂ h₁,
  integralSum, integralSum, Finset.sum_sub_distrib]
no goals
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : IsPartition π₁
h₂ : IsPartition π₂
⊢ ∑ J in (infPrepartition π₁ π₂.toPrepartition).toPrepartition.boxes,
        ↑(↑vol J) (f (tag (infPrepartition π₁ π₂.toPrepartition) J)) -
      ∑ J in (infPrepartition π₂ π₁.toPrepartition).toPrepartition.boxes,
        ↑(↑vol J) (f (tag (infPrepartition π₂ π₁.toPrepartition) J)) =
    ∑ x in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ↑(↑vol x) (f (tag (infPrepartition π₁ π₂.toPrepartition) x)) -
      ∑ x in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ↑(↑vol x) (f (tag (infPrepartition π₂ π₁.toPrepartition) x))
simp only [infPrepartition_toPrepartition, inf_comm]