awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
have inl : ∀ (hs : Convex.{0, u_2} ℝ (E := E) ∅) (hω : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt ω (dω x) ∅ x)
  (hdω :
    ∀ (a : E),
      Membership.mem (γ := Set E) ∅ a →
        ∀ x ∈ tangentConeAt ℝ ∅ a,
          ∀ y ∈ tangentConeAt ℝ ∅ a,
            Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
              ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)),
  ∃ (f : E → F), ∀ (a : E), Membership.mem (γ := Set E) ∅ a → HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) ∅ a
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
Cleared hypotheses: s, hs, hω, hdω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
inl :
  ∀ (hs : Convex.{0, u_2} ℝ (E := E) ∅)
    (hω : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt ω (dω x) ∅ x)
    (hdω :
      ∀ (a : E),
        Membership.mem (γ := Set E) ∅ a →
          ∀ x ∈ tangentConeAt ℝ ∅ a,
            ∀ y ∈ tangentConeAt ℝ ∅ a,
              Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
                ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)),
    ∃ (f : E → F), ∀ (a : E), Membership.mem (γ := Set E) ∅ a → HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) ∅ a
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
have inr : ∀ (a : E) (ha : a ∈ s), ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
have h : ∀ a_1 ∈ s,
  HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ curveIntegral ω (Path.segment a x)) (ω a_1) s a_1
Tactic: use (curveIntegral ω <| .segment a ·)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
have refine : ∀ (a : E) (ha : a ∈ s),
  ∀ x ∈ tangentConeAt ℝ s a,
    ∀ y ∈ tangentConeAt ℝ s a,
      Eq.{u_3 + 1} (α := F) ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
Tactic: refine hs.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric hω fun a ha x _ y _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
x : E
h : x ∈ tangentConeAt ℝ s a
y : E
h_1 : y ∈ tangentConeAt ℝ s a
⊢ Eq.{u_3 + 1} (α := F) ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
    ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
have hs₁ : UniqueDiffWithinAt ℝ s a
Tactic: rw [fderivWithin_eq_fderiv, hdω a ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
x : E
h : x ∈ tangentConeAt ℝ s a
y : E
h_1 : y ∈ tangentConeAt ℝ s a
hs₁ : UniqueDiffWithinAt ℝ s a
⊢ Eq.{u_3 + 1} (α := F) ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
    ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
have h : DifferentiableAt ℝ ω a
Tactic: rw [fderivWithin_eq_fderiv, hdω a ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) a
have obtain : ∀ (f : E → F) (hf : ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a),
  ∃ (f : E → F), ∀ a ∈ s, HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) a
Tactic: obtain ⟨f, hf⟩ : ∃ f, ∀ a ∈ s, HasFDerivWithinAt f (ω a) s a := by
    refine hs.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric hω fun a ha x _ y _ ↦ ?_
    rw [fderivWithin_eq_fderiv, hdω a ha]
    exacts [hso.uniqueDiffOn a ha, hω.differentiableAt (hso.mem_nhds ha)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ ∃ (g : 𝕜 → E), ∀ a ∈ s, HasDerivWithinAt g (f a) s a
have hω : ∀ x ∈ s,
  HasFDerivWithinAt (𝕜 := ℝ) (F := 𝕜 →L[𝕜] E) (fun (a : 𝕜) ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a))
    (ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
      (ContinuousLinearMap.toSpanSingleton 𝕜
        (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 : (a : E) → 𝕜 →L[𝕜] E)
          (derivWithin f s x))))
    s x
Tactic: apply hs.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hω :
  ∀ x ∈ s,
    HasFDerivWithinAt (𝕜 := ℝ) (F := 𝕜 →L[𝕜] E) (fun (a : 𝕜) ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a))
      (ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
        (ContinuousLinearMap.toSpanSingleton 𝕜
          (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 : (a : E) → 𝕜 →L[𝕜] E)
            (derivWithin f s x))))
      s x
⊢ ∃ (g : 𝕜 → E), ∀ a ∈ s, HasDerivWithinAt g (f a) s a
have hdω : ∀ a ∈ s,
  ∀ x ∈ tangentConeAt ℝ s a,
    ∀ y ∈ tangentConeAt ℝ s a,
      Eq.{u_2 + 1} (α := E)
        (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                        (ContinuousLinearMap.toSpanSingleton 𝕜
                          (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                              (a : E) → 𝕜 →L[𝕜] E)
                            (derivWithin f s a))) :
                      𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                    (a : 𝕜) → 𝕜 →L[𝕜] E)
                  x :
                𝕜 →L[𝕜] E) :
              (a : 𝕜) → E)
            y :
          E)
        (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                        (ContinuousLinearMap.toSpanSingleton 𝕜
                          (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                              (a : E) → 𝕜 →L[𝕜] E)
                            (derivWithin f s a))) :
                      𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                    (a : 𝕜) → 𝕜 →L[𝕜] E)
                  y :
                𝕜 →L[𝕜] E) :
              (a : 𝕜) → E)
            x :
          E)
Tactic: apply hs.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hω :
  ∀ x ∈ s,
    HasFDerivWithinAt (𝕜 := ℝ) (F := 𝕜 →L[𝕜] E) (fun (a : 𝕜) ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a))
      (ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
        (ContinuousLinearMap.toSpanSingleton 𝕜
          (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 : (a : E) → 𝕜 →L[𝕜] E)
            (derivWithin f s x))))
      s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_2 + 1} (α := E)
          (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                          (ContinuousLinearMap.toSpanSingleton 𝕜
                            (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                                (a : E) → 𝕜 →L[𝕜] E)
                              (derivWithin f s a))) :
                        𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                      (a : 𝕜) → 𝕜 →L[𝕜] E)
                    x :
                  𝕜 →L[𝕜] E) :
                (a : 𝕜) → E)
              y :
            E)
          (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                          (ContinuousLinearMap.toSpanSingleton 𝕜
                            (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                                (a : E) → 𝕜 →L[𝕜] E)
                              (derivWithin f s a))) :
                        𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                      (a : 𝕜) → 𝕜 →L[𝕜] E)
                    y :
                  𝕜 →L[𝕜] E) :
                (a : 𝕜) → E)
              x :
            E)
⊢ ∃ (g : 𝕜 → E), ∀ a ∈ s, HasDerivWithinAt g (f a) s a
have apply : 𝕜 → 𝕜 →L[ℝ] 𝕜 →L[𝕜] E
Tactic: apply hs.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ 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))
have 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))
Tactic: simp only [← setIntegral_congr_set (Box.coe_ae_eq_Icc _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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
⊢ 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))
have 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)
Tactic: have A := (Hi.mono_set Box.coe_subset_Icc).hasBoxIntegral ⊥ rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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
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
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)
⊢ 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))
have 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) → ℝ))
Tactic: have hJ_sub' : ∀ k, Box.Icc (J k) ⊆ Box.Icc I := fun k => (hJ_sub k).trans I.Ioo_subset_Icc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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
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
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) → ℝ))
⊢ 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))
have hJ_le : ∀ (k : ℕ), (J : (a : ℕ) → Box (Fin (n + 1))) k ≤ I
Tactic: have hJ_le : ∀ k, J k ≤ I := fun k => Box.le_iff_Icc.2 (hJ_sub' k)