awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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
⊢ 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
have this₁ : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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] ∅
⊢ 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
have 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
Tactic: rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,
        setIntegral_empty, sub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ 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
have 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
Tactic: rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,
        setIntegral_empty, sub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ 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
have 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
Tactic: rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,
        setIntegral_empty, sub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ 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
have inl₃ : HSub.hSub (α := E) 0 0 = 0
Tactic: rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,
        setIntegral_empty, sub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ 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
have inl₄ : Eq.{u + 1} (α := E) 0 0
Tactic: rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,
        setIntegral_empty, sub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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
⊢ 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))
have hlt : ∀ (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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
⊢ Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
have h : ∀ (x : F),
  Membership.mem (γ := Set F)
      (Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
        (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)))
      x ↔
    x ∈ Set.Icc a b
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
⊢ Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
have rw : Eq (α := Set (Fin (n + 1) → ℝ))
  (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
  (Set.preimage (β := F) (⇑eL.symm : (a : Fin (n + 1) → ℝ) → F)
      (Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
        (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))) :
    Set (Fin (n + 1) → ℝ))
Tactic: rw [← hIcc, eL.symm_preimage_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
rw :
  Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    (Set.preimage (β := F) (⇑eL.symm : (a : Fin (n + 1) → ℝ) → F)
        (Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
          (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))) :
      Set (Fin (n + 1) → ℝ))
⊢ Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
have rw₁ : Eq (α := Set (Fin (n + 1) → ℝ))
  (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
  (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
Tactic: rw [← hIcc, eL.symm_preimage_preimage]