Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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 : s.Countable
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.upper i) x) i

pp: case refine_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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 : s.Countable
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i

Tactic:
· have := Box.continuousOn_face_Icc (Hc i) (Set.right_mem_Icc.2 (I.lower_le_upper i))
    have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set
      Box.coe_subset_Icc
    exact (this.hasBoxIntegral ⊥ rfl).integral_eq

Goal state after:
case refine_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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 : s.Countable
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i