Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : Box.Icc J ⊆ Set.univ.pi fun i ↦ Set.Icc (I₀.lower i) (I₀.upper i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : ↑(J.face i) ≤ ↑(I₀.face i)
hx' : x ∈ Set.Ioo ((J.face i).lower j) ((J.face i).upper j)
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower (i.succAbove j) x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper (i.succAbove j) x) =
    Option.elim' 0 (⇑(fb ⟨J.upper i, ⋯⟩)) ((J.face i).splitLower j x) +
        Option.elim' 0 (⇑(fb ⟨J.upper i, ⋯⟩)) ((J.face i).splitUpper j x) -
      (Option.elim' 0 (⇑(fb ⟨J.lower i, ⋯⟩)) ((J.face i).splitLower j x) +
        Option.elim' 0 (⇑(fb ⟨J.lower i, ⋯⟩)) ((J.face i).splitUpper j x))

Tactic:
simp only [Box.splitLower_def hx, Box.splitUpper_def hx, Box.splitLower_def hx',
          Box.splitUpper_def hx', ← WithBot.some_eq_coe, Option.elim', Box.face_mk,
          update_of_ne (Fin.succAbove_ne _ _).symm, sub_add_sub_comm,
          update_comp_eq_of_injective _ (Fin.strictMono_succAbove i).injective j x, ← hf]

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : Box.Icc J ⊆ Set.univ.pi fun i ↦ Set.Icc (I₀.lower i) (I₀.upper i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : ↑(J.face i) ≤ ↑(I₀.face i)
hx' : x ∈ Set.Ioo ((J.face i).lower j) ((J.face i).upper j)
⊢ f (J.upper i) { lower := J.lower ∘ i.succAbove, upper := update (J.upper ∘ i.succAbove) j x, lower_lt_upper := ⋯ } +
        f (J.upper i)
          { lower := update (J.lower ∘ i.succAbove) j x, upper := J.upper ∘ i.succAbove, lower_lt_upper := ⋯ } -
      (f (J.lower i)
          { lower := J.lower ∘ i.succAbove, upper := update (J.upper ∘ i.succAbove) j x, lower_lt_upper := ⋯ } +
        f (J.lower i)
          { lower := update (J.lower ∘ i.succAbove) j x, upper := J.upper ∘ i.succAbove, lower_lt_upper := ⋯ }) =
    f (J.upper i) { lower := (J.face i).lower, upper := update (J.face i).upper j x, lower_lt_upper := ⋯ } +
        f (J.upper i) { lower := update (J.face i).lower j x, upper := (J.face i).upper, lower_lt_upper := ⋯ } -
      (f (J.lower i) { lower := (J.face i).lower, upper := update (J.face i).upper j x, lower_lt_upper := ⋯ } +
        f (J.lower i) { lower := update (J.face i).lower j x, upper := (J.face i).upper, lower_lt_upper := ⋯ })