E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑Box.Icc I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in ↑Box.Icc (Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i) -
        ∫ (x : Fin n → ℝ) in ↑Box.Icc (Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i)
simp only [← set_integral_congr_set_ae (Box.coe_ae_eq_Icc _)]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
have A := (Hi.mono_set Box.coe_subset_Icc).hasBoxIntegral ⊥ rfl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
have B :=
  hasIntegral_GP_divergence_of_forall_hasDerivWithinAt I f f' (s ∩ Box.Icc I)
    (hs.mono (inter_subset_left _ _)) (fun x hx => Hc _ hx.2) fun x hx =>
    Hd _ ⟨hx.1, fun h => hx.2 ⟨h, hx.1⟩⟩
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ContinuousOn f (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
rw [continuousOn_pi] at Hc
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
        BoxAdditiveMap.volume -
      BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
        BoxAdditiveMap.volume =
    (∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i) -
      ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
⊢ (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ x_1 : Fin (n + 1), ↑(f' x) (e x_1) x_1) =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.upper I x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(Box.face I x), f (Fin.insertNth x (Box.lower I x) x_1) x)
refine' (A.unique B).trans (sum_congr rfl fun i _ => _)
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i

case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
        BoxAdditiveMap.volume -
      BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
        BoxAdditiveMap.volume =
    (∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i) -
      ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
refine' congr_arg₂ Sub.sub _ _
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.upper I i)) (↑Box.Icc (Box.face I i))
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i
have := Box.continuousOn_face_Icc (Hc i) (Set.right_mem_Icc.2 (I.lower_le_upper i))
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this✝ : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.upper I i)) (↑Box.Icc (Box.face I i))
this : IntegrableOn ((fun y => f y i) ∘ Fin.insertNth i (Box.upper I i)) ↑(Box.face I i)
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.upper I i)) (↑Box.Icc (Box.face I i))
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i
have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set
  Box.coe_subset_Icc
no goals
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this✝ : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.upper I i)) (↑Box.Icc (Box.face I i))
this : IntegrableOn ((fun y => f y i) ∘ Fin.insertNth i (Box.upper I i)) ↑(Box.face I i)
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.upper I i) x) i
exact (this.hasBoxIntegral ⊥ rfl).integral_eq
case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.lower I i)) (↑Box.Icc (Box.face I i))
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
have := Box.continuousOn_face_Icc (Hc i) (Set.left_mem_Icc.2 (I.lower_le_upper i))
case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this✝ : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.lower I i)) (↑Box.Icc (Box.face I i))
this : IntegrableOn ((fun y => f y i) ∘ Fin.insertNth i (Box.lower I i)) ↑(Box.face I i)
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.lower I i)) (↑Box.Icc (Box.face I i))
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set
  Box.coe_subset_Icc
no goals
case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (↑Box.Icc I)
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (↑Box.Icc I)
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), ↑(f' x) (e i) i)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this✝ : ContinuousOn ((fun y => f y i) ∘ Fin.insertNth i (Box.lower I i)) (↑Box.Icc (Box.face I i))
this : IntegrableOn ((fun y => f y i) ∘ Fin.insertNth i (Box.lower I i)) ↑(Box.face I i)
⊢ BoxIntegral.integral (Box.face I i) IntegrationParams.GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(Box.face I i), f (Fin.insertNth i (Box.lower I i) x) i
exact (this.hasBoxIntegral ⊥ rfl).integral_eq