-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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 : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivAt (𝕜 := ℝ) f (f' x) x
J : ℕ →o Box (Fin (n + 1))
hJ_sub :
  ∀ (n_1 : ℕ),
    Subset (α := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
          ((J : (a : ℕ) → Box (Fin (n + 1))) n_1 : Box (Fin (n + 1))) :
        Set (Fin (n + 1) → ℝ))
      ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ))
hJl : Tendsto (α := ℕ) (Box.lower ∘ (⇑J : (a : ℕ) → Box (Fin (n + 1)))) atTop (𝓝 I.lower)
hJu : Tendsto (α := ℕ) (Box.upper ∘ (⇑J : (a : ℕ) → Box (Fin (n + 1)))) atTop (𝓝 I.upper)
hJ_sub' :
  ∀ (k : ℕ),
    Subset (α := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
          ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))) :
        Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ))
hJ_le : ∀ (k : ℕ), (J : (a : ℕ) → Box (Fin (n + 1))) k ≤ I
HcJ :
  ∀ (k : ℕ),
    ContinuousOn f
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
        ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))))
HdJ :
  ∀ (k : ℕ) (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
              ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))) \
            s :
          Set (Fin (n + 1) → ℝ))
        x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x)
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
          ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))))
        x
HiJ :
  ∀ (k : ℕ),
    IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
        ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))))
      volume
HJ_eq :
  ∀ (k : ℕ),
    Eq.{u + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
            ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1)))))
        fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
      (∑ i : Fin (n + 1),
        HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume
              ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i)))
            fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (Box.upper ((J : (a : ℕ) → Box (Fin (n + 1))) k) i) x) i)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume
              ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i)))
            fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (Box.lower ((J : (a : ℕ) → Box (Fin (n + 1))) k) i) x) i))
Hi :
  @Integrable.{u, 0} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : Fin (n + 1),
        (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
    (Measure.restrict volume ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I))
rw :
  ∀
    (Hi :
      @Integrable.{u, 0} E _ _ _ MeasureSpace.toMeasurableSpace
        (fun (x : Fin (n + 1) → ℝ) ↦
          ∑ i : Fin (n + 1),
            (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
        (Measure.restrict volume
          (⋃ (n_1 : ℕ),
            (Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
              ((J : (a : ℕ) → Box (Fin (n + 1))) n_1 : Box (Fin (n + 1)))))),
    Tendsto.{0, u} (β := E)
      (fun (k : ℕ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
              ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1)))))
          fun (x : Fin (n + 1) → ℝ) ↦
          ∑ i : Fin (n + 1),
            (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
      atTop
      (𝓝
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (⋃ (n_1 : ℕ),
              (Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
                ((J : (a : ℕ) → Box (Fin (n + 1))) n_1 : Box (Fin (n + 1)))))
          fun (x : Fin (n + 1) → ℝ) ↦
          ∑ i : Fin (n + 1),
            (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i))
⊢ Tendsto.{0, u} (β := E)
    (fun (k : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
            ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1)))))
        fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I))
        fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i))

Tactic:
rw [← Box.iUnion_Ioo_of_tendsto J.monotone hJl hJu] at Hi ⊢

Premises used: OrderHom.monotone, BoxIntegral.Box.iUnion_Ioo_of_tendsto