-- Mathlib/Analysis/BoxIntegral/Partition/Additive.lean
theorem sum_boxes_congr [Finite ι] (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) {π₁ π₂ : Prepartition I}
    (h : π₁.iUnion = π₂.iUnion) : ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Proof state:
case intro.calc_1
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₁.boxes
⊢ ↑J ≤ I₀

case intro.calc_2
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
⊢ ↑J ≤ I₀

Tactic:
exacts [(WithTop.coe_le_coe.2 <| π₁.le_of_mem hJ).trans hI,
  (WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI]

Result:
no goals

Proof state:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
rw [h] at h₁

Result:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Proof state:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
simp only [inf_splitMany] at hs

Result:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
rcases exists_splitMany_inf_eq_filter_of_finite {π₁, π₂} ((finite_singleton _).insert _) with
  ⟨s, hs⟩

Result:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ (π₁.biUnion fun J => splitMany J s).boxes, f J = ∑ J ∈ (π₂.biUnion fun J => splitMany J s).boxes, f J

Tactic:
rw [h₁, h₂]

Result:
no goals

Proof state:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
calc
  ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₁.boxes, ∑ J' ∈ (splitMany J s).boxes, f J' :=
    Finset.sum_congr rfl fun J hJ => (f.sum_partition_boxes ?_ (isPartition_splitMany _ _)).symm
  _ = ∑ J ∈ (π₁.biUnion fun J => splitMany J s).boxes, f J := (sum_biUnion_boxes _ _ _).symm
  _ = ∑ J ∈ (π₂.biUnion fun J => splitMany J s).boxes, f J := by rw [h₁, h₂]
  _ = ∑ J ∈ π₂.boxes, ∑ J' ∈ (splitMany J s).boxes, f J' := sum_biUnion_boxes _ _ _
  _ = ∑ J ∈ π₂.boxes, f J :=
    Finset.sum_congr rfl fun J hJ => f.sum_partition_boxes ?_ (isPartition_splitMany _ _)

Result:
case intro.calc_1
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₁.boxes
⊢ ↑J ≤ I₀

case intro.calc_2
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
⊢ ↑J ≤ I₀

Proof state:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
rcases hs _ (Or.inl rfl), hs _ (Or.inr rfl) with ⟨h₁, h₂⟩

Result:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J