-- 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_1 : ι
G : Type u
inst_2 : 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)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ :
  Subset (α := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ))
    (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Icc (I₀.lower i) (I₀.upper i) :
      Set ((i : Fin (n + 1)) → ℝ))
j_1 : 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) : WithTop (Box (Fin n))) ≤ (↑(I₀.face i) : WithTop (Box (Fin n)))
hx' : x ∈ Set.Ioo ((J.face i).lower j) ((J.face i).upper j)
refine_2 :
  f (J.upper i)
          { lower := J.lower ∘ i.succAbove, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.upper ∘ i.succAbove) j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.upper i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.lower ∘ i.succAbove) j x, upper := J.upper ∘ i.succAbove,
            lower_lt_upper := ⋯ : Box (Fin n) } -
      (f (J.lower i)
          { lower := J.lower ∘ i.succAbove, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.upper ∘ i.succAbove) j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.lower i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.lower ∘ i.succAbove) j x, upper := J.upper ∘ i.succAbove,
            lower_lt_upper := ⋯ : Box (Fin n) }) =
    f (J.upper i)
          { lower := (J.face i).lower, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).upper j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.upper i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).lower j x, upper := (J.face i).upper,
            lower_lt_upper := ⋯ : Box (Fin n) } -
      (f (J.lower i)
          { lower := (J.face i).lower, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).upper j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.lower i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).lower j x, upper := (J.face i).upper,
            lower_lt_upper := ⋯ : Box (Fin n) })
⊢ HAdd.hAdd (α := G)
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ 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 : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitUpper (i.succAbove j) x)) =
    HAdd.hAdd (α := G)
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.upper i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((J.face i).splitLower j x))
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.upper i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((J.face i).splitUpper j x)) -
      HAdd.hAdd (α := G)
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.lower i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((J.face i).splitLower j x))
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.lower i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((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]

Premises used: Iff.mpr, BoxIntegral.Box.splitLower_def, Option.elim', Fin.strictMono_succAbove, BoxIntegral.Box.face_mk, BoxIntegral.Box.splitUpper_def, Fin.succAbove_ne, BoxIntegral.Box.upper, Ne.symm, sub_add_sub_comm, StrictMono.injective, BoxIntegral.Box.lower, And.right, Function.forall_update_iff, And.left, WithBot.some_eq_coe, And.intro, LT.lt, BoxIntegral.Box.lower_lt_upper, Function.update_comp_eq_of_injective, Function.update_of_ne