awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
⊢ Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅

Tactic:
have : (pi Set.univ fun j => Ioc (a j) (b j)) = ∅ := univ_pi_eq_empty hi'
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
inl :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ x →
      HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume (Set.Icc (a ∘ x.succAbove) (b ∘ x.succAbove))) fun (x_1 : Fin n → ℝ) ↦
            f (x.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b x) x_1) x)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume (Set.Icc (a ∘ x.succAbove) (b ∘ x.succAbove))) fun (x_1 : Fin n → ℝ) ↦
            f (x.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a x) x_1) x) =
        0
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : Fin (n + 1)) ↦ ℝ))
      (Measure.restrict (Measure.pi (α := fun (a : Fin (n + 1)) ↦ ℝ) fun (x : Fin (n + 1)) ↦ volume)
        (Set.pi (α := fun (a : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioc (a i) (b i)))
      fun (x : (i : 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 (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i))

Tactic:
rw [this, setIntegral_empty, sum_eq_zero]

Premises used: Finset.sum_eq_zero, MeasureTheory.setIntegral_empty
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
j : Fin (n + 1)
inl :
  HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i) =
    0
inl₁ :
  ∀ (hne : i ≠ j),
    HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
          f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b j) x) j)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
          f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
      0
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b j) x) j)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
    0

Tactic:
rcases eq_or_ne i j with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i) =
    0

Tactic:
simp [hi]
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
j : Fin (n + 1)
hne : i ≠ j
inl :
  ∀ (i : Fin n) (hi : a (j.succAbove i) = b (j.succAbove i)) (hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅)
    (hne : j.succAbove i ≠ j),
    HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
          f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b j) x) j)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
          f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
      0
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b j) x) j)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
    0

Tactic:
rcases Fin.exists_succAbove_eq hne with ⟨i, rfl⟩

Premises used: Fin.exists_succAbove_eq, rfl
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
this :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
rw : ENNReal.ofReal ((b ∘ j.succAbove) i - (a ∘ j.succAbove) i) = 0
⊢ Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᶠ[ae (F := Measure (Fin n → ℝ)) volume] ∅

Tactic:
rw [ae_eq_empty, Real.volume_Icc_pi, prod_eq_zero (Finset.mem_univ i)]

Premises used: Finset.mem_univ, Real.volume_Icc_pi, MeasureTheory.ae_eq_empty, Finset.prod_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
this :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
⊢ ENNReal.ofReal ((b ∘ j.succAbove) i - (a ∘ j.succAbove) i) = 0

Tactic:
simp [hi]
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
this :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
⊢ Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᶠ[ae (F := Measure (Fin n → ℝ)) volume] ∅

Tactic:
have : Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] (∅ : Set ℝⁿ) := by
        rw [ae_eq_empty, Real.volume_Icc_pi, prod_eq_zero (Finset.mem_univ i)]
        simp [hi]
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
this_1 :
  Eq (α := Set ((i : Fin (n + 1)) → ℝ))
    (Set.pi (α := fun (j : Fin (n + 1)) ↦ ℝ) Set.univ fun (j : Fin (n + 1)) ↦ Set.Ioc (a j) (b j)) ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
this : Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᶠ[ae (F := Measure (Fin n → ℝ)) volume] ∅
inl :
  HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ∅) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b j) x) j)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
    0
inl₁ :
  HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ∅) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b j) x) j)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ∅) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
    0
inl₂ :
  HSub.hSub (α := E) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ∅) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
    0
inl₃ : HSub.hSub (α := E) 0 0 = 0
inl₄ inl₅ : Eq.{u + 1} (α := E) 0 0
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b j) x) j)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume (Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove))) fun (x : Fin n → ℝ) ↦
        f (j.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a j) x) j) =
    0

Tactic:
rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,
        setIntegral_empty, sub_self]

Premises used: sub_self, MeasureTheory.setIntegral_empty, MeasureTheory.setIntegral_congr_set
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
hne : ¬∃ (i : Fin (n + 1)), a i = b i
⊢ ∀ (i : Fin (n + 1)), a i < b i

Tactic:
have hlt : ∀ i, a i < b i := fun i => (hle i).lt_of_ne fun hi => hne ⟨i, hi⟩
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
hne : ¬∃ (i : Fin (n + 1)), a i = b i
hlt : ∀ (i : Fin (n + 1)), a i < b i
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b))
      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 (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i))

Tactic:
integral_divergence_of_hasFDerivAt_off_countable_aux₂ ⟨a, b, hlt⟩ f f' s hs Hc Hd Hi

Premises used: setOf, Set.Icc, _private.0.MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_aux₂, BoxIntegral.Box.mk
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) 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)
    (Set.Icc a b) volume
hne : ¬∃ (i : Fin (n + 1)), a i = b i
hlt : ∀ (i : Fin (n + 1)), a i < b i
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b))
      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 (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i))

Tactic:
exact integral_divergence_of_hasFDerivAt_off_countable_aux₂ ⟨a, b, hlt⟩ f f' s hs Hc Hd Hi

Premises used: _private.0.MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_aux₂, BoxIntegral.Box.mk
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : Fin (n + 1) → (Fin (n + 1) → ℝ) → E
f' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd :
  ∀ x ∈ (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : Fin (n + 1), (f' i x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
    (Set.Icc a b) volume
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b))
      fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : Fin (n + 1), (f' i x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f i (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f i (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x)))

Tactic:
integral_divergence_of_hasFDerivAt_off_countable a b hle (fun x i => f i x)
    (fun x => ContinuousLinearMap.pi fun i => f' i x) s hs (continuousOn_pi.2 Hc)
    (fun x hx => hasFDerivAt_pi.2 (Hd x hx)) Hi

Premises used: Iff.mpr, ContinuousLinearMap.pi, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, continuousOn_pi, hasFDerivAt_pi