-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀_1 : WithTop (Box ι)
I : Box ι
i : ι
inst_2 : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    (↑I : WithTop (Box ι)) ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
refine : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₁ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₂ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (π : Prepartition I) (hπ : π.IsPartition), ∑ Ji ∈ π.boxes, f Ji = f I
refine₃ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (π : Prepartition I) (hπ : π.IsPartition)
    (Hle : ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀), ∑ Ji ∈ π.boxes, f Ji = f I
refine₄ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (π : Prepartition I) (hπ : π.IsPartition)
    (Hle : ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)) (hs : splitMany I s ≤ π),
    ∑ Ji ∈ π.boxes, f Ji = f I
refine₅ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (π : Prepartition I) (hπ : π.IsPartition)
    (Hle : ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)) (hs : splitMany I s ≤ π),
    Eq.{u_2 + 1} (α := M) (∑ Ji ∈ π.boxes, f Ji) (∑ J ∈ π.boxes, ∑ J' ∈ (splitMany J s).boxes, f J')
⊢ ι →ᵇᵃ[I₀] M

Tactic:
classical
  refine ⟨f, ?_⟩
  replace hf (I : Box ι) (hI : ↑I ≤ I₀) (s) : ∑ J ∈ (splitMany I s).boxes, f J = f I := by
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s _ ihs =>
      rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
      refine Finset.sum_congr rfl fun J' hJ' => ?_
      by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
      · rw [sum_split_boxes]
        exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h
      · rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
  intro I hI π hπ
  have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
  rcases hπ.exists_splitMany_le with ⟨s, hs⟩
  rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
  exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm

Premises used: BoxIntegral.Prepartition.sum_biUnion_boxes, BoxIntegral.Prepartition.biUnion_boxes, BoxIntegral.Prepartition.inf_splitMany