awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
this :
  ∀ (hE : CompleteSpace E),
    Eq.{u + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume ((Box.Icc : (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)
      (∑ i : Fin (n + 1),
        HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))) fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))) fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i))
hE : ¬CompleteSpace E
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume ((Box.Icc : (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)
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i))

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
simp :
  Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (↑I : Set (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)
    (∑ x : Fin (n + 1),
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (↑(I.face x) : Set (Fin n → ℝ)))
          fun (x_1 : Fin n → ℝ) ↦ f (x.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper x) x_1) x)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (↑(I.face x) : Set (Fin n → ℝ)))
          fun (x_1 : Fin n → ℝ) ↦ f (x.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower x) x_1) x))
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume ((Box.Icc : (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)
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i))

Tactic:
simp only [← setIntegral_congr_set (Box.coe_ae_eq_Icc _)]

Premises used: BoxIntegral.Box.coe_ae_eq_Icc, MeasureTheory.setIntegral_congr_set
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
⊢ HasIntegral.{0, u, u} (E := E) 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)
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict volume (↑I : Set (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)

Tactic:
have A := (Hi.mono_set Box.coe_subset_Icc).hasBoxIntegral ⊥ rfl
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
A :
  HasIntegral.{0, u, u} (E := E) 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)
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict volume (↑I : Set (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)
⊢ HasIntegral.{0, u, u} (E := E) I IntegrationParams.GP
    (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)
    BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
          BoxAdditiveMap.volume)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
          BoxAdditiveMap.volume))

Tactic:
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⟩⟩
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
A :
  HasIntegral.{0, u, u} (E := E) 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)
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict volume (↑I : Set (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)
B :
  HasIntegral.{0, u, u} (E := E) I IntegrationParams.GP
    (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)
    BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
          BoxAdditiveMap.volume)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
          BoxAdditiveMap.volume))
⊢ ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (Y := E) (fun (y : Fin (n + 1) → ℝ) ↦ f y i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
rw [continuousOn_pi] at Hc

Premises used: continuousOn_pi
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
A :
  HasIntegral.{0, u, u} (E := E) 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)
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict volume (↑I : Set (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)
B :
  HasIntegral.{0, u, u} (E := E) I IntegrationParams.GP
    (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)
    BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
          BoxAdditiveMap.volume)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
          BoxAdditiveMap.volume))
Hc₁ :
  ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (Y := E) (fun (y : Fin (n + 1) → ℝ) ↦ f y i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x

Tactic:
rw [continuousOn_pi] at Hc

Premises used: continuousOn_pi
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
A :
  HasIntegral.{0, u, u} (E := E) 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)
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict volume (↑I : Set (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)
B :
  HasIntegral.{0, u, u} (E := E) I IntegrationParams.GP
    (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)
    BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
          BoxAdditiveMap.volume)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
          BoxAdditiveMap.volume))
Hc₁ :
  ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (Y := E) (fun (y : Fin (n + 1) → ℝ) ↦ f y i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hd₁ :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
⊢ 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) → ℝ)) I) volume

Tactic:
rw [continuousOn_pi] at Hc

Premises used: continuousOn_pi
-- 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.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
A :
  HasIntegral.{0, u, u} (E := E) 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)
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict volume (↑I : Set (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)
B :
  HasIntegral.{0, u, u} (E := E) I IntegrationParams.GP
    (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)
    BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
          BoxAdditiveMap.volume)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
          BoxAdditiveMap.volume))
Hc₁ :
  ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (Y := E) (fun (y : Fin (n + 1) → ℝ) ↦ f y i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hd₁ :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi₁ :
  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) → ℝ)) I) volume
⊢ CompleteSpace E

Tactic:
rw [continuousOn_pi] at Hc

Premises used: continuousOn_pi
-- 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 :
  ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (Y := E) (fun (y : Fin (n + 1) → ℝ) ↦ f y i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hi :
  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) → ℝ)) I) volume
hE : CompleteSpace E
A :
  HasIntegral.{0, u, u} (E := E) 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)
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict volume (↑I : Set (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)
B :
  HasIntegral.{0, u, u} (E := E) I IntegrationParams.GP
    (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)
    BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x) i)
          BoxAdditiveMap.volume)
        (BoxIntegral.integral (I.face i) IntegrationParams.GP
          (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ ContinuousOn.{0, u} (X := (j : Fin n) → ℝ) (Y := E)
    ((fun (y : Fin (n + 1) → ℝ) ↦ f y i) ∘ i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) :
      ((j : Fin n) → ℝ) → E)
    ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))

Tactic:
have := Box.continuousOn_face_Icc (Hc i) (Set.right_mem_Icc.2 (I.lower_le_upper i))