case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} → π ⊓ splitMany I s = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
rcases exists_splitMany_inf_eq_filter_of_finite {π₁, π₂} ((finite_singleton _).insert _) with
  ⟨s, hs⟩
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} →
      (biUnion π fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} → π ⊓ splitMany I s = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
simp only [inf_splitMany] at hs
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} →
      (biUnion π fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₁
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} →
      (biUnion π fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
rcases hs _ (Or.inl rfl), hs _ (Or.inr rfl) with ⟨h₁, h₂⟩
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₁
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} →
      (biUnion π fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₁
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
clear hs
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₁
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
rw [h] at h₁
case intro.calc_1
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J✝ : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₁.boxes
⊢ ↑J ≤ I₀

case intro.calc_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J✝ : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₂.boxes
⊢ ↑J ≤ I₀
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
calc
  (∑ J in π₁.boxes, f J) = ∑ J in π₁.boxes, ∑ J' in (splitMany J s).boxes, f J' :=
    Finset.sum_congr rfl fun J hJ => (f.sum_partition_boxes ?_ (isPartition_splitMany _ _)).symm
  _ = ∑ J in (π₁.biUnion fun J => splitMany J s).boxes, f J := (sum_biUnion_boxes _ _ _).symm
  _ = ∑ J in (π₂.biUnion fun J => splitMany J s).boxes, f J := by rw [h₁, h₂]
  _ = ∑ J in π₂.boxes, ∑ J' in (splitMany J s).boxes, f J' := (sum_biUnion_boxes _ _ _)
  _ = ∑ J in π₂.boxes, f J :=
    Finset.sum_congr rfl fun J hJ => f.sum_partition_boxes ?_ (isPartition_splitMany _ _)
no goals
case intro.calc_1
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J✝ : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₁.boxes
⊢ ↑J ≤ I₀

case intro.calc_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J✝ : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₂.boxes
⊢ ↑J ≤ I₀
exacts [(WithTop.coe_le_coe.2 <| π₁.le_of_mem hJ).trans hI,
  (WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI]
no goals
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.77819
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in (biUnion π₁ fun J => splitMany J s).boxes, ↑f J = ∑ J in (biUnion π₂ fun J => splitMany J s).boxes, ↑f J
rw [h₁, h₂]