awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
refine_1 : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] ℝ
refine_2 :
  ∀ (J : Box (Fin (n + 1))),
    LE.le (α := ℝ) (0 : ℝ)
      ((BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) (↑I : WithTop (Box (Fin (n + 1)))) ⋯ :
            (a : Box (Fin (n + 1))) → ℝ)
          J :
        ℝ)
⊢ HasIntegral (E := E) (F := E) I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
    (BoxAdditiveMap.volume : Fin (n + 1) →ᵇᵃ[⊤] E →L[ℝ] E) ((F : (a : Box (Fin (n + 1))) → E) I : E)
have refine_3 : ∀ (c : ℝ≥0) (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 →
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ J ≤ I,
          (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J ⊆ closedBall x δ →
            Membership.mem (γ := Set (Fin (n + 1) → ℝ))
                ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ)) x →
              (GP.bDistortion = true → J.distortion ≤ c) →
                dist (α := E)
                    ((((BoxAdditiveMap.volume : (a : Box (Fin (n + 1))) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E)
                        ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) :
                      E)
                    ((F : (a : Box (Fin (n + 1))) → E) J : E) ≤
                  ε
Tactic: refine HasIntegral.of_le_Henstock_of_forall_isLittleO gp_le ?_ ?_ _ s hs ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
          ∀ y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
            ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) *
            norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) ≤
          ε / 2
have refine_1 : ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
  ∀ y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
    ∀ y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I, ‖f y₁ - f y₂‖ ≤ ε / 2
Tactic: refine .and (Ioc_mem_nhdsGT one_half_pos) (.and ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
refine_1 :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    ∀ y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
      ∀ y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I, ‖f y₁ - f y₂‖ ≤ ε / 2
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
          ∀ y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
            ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) *
            norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) ≤
          ε / 2
have refine_2 : ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
  (2 * δ) ^ (n + 1) *
      norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) ≤
    ε / 2
Tactic: refine .and (Ioc_mem_nhdsGT one_half_pos) (.and ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    ∀ y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
      ∀ y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I, ‖f y₁ - f y₂‖ ≤ ε / 2
have refine_1 : ∀ (δ₁ : ℝ) (δ₁0 : 0 < δ₁)
  (hδ₁ :
    ∀ x_1 ∈ closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
      f x_1 ∈ closedBall (f x) (ε / 2 / 2)),
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    ∀ y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
      ∀ y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I, ‖f y₁ - f y₂‖ ≤ ε / 2
Tactic: rcases ((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_closedBall).1
            (Hs x hx.2) _ (half_pos <| half_pos ε0) with ⟨δ₁, δ₁0, hδ₁⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ :
  ∀ x_1 ∈ closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
    f x_1 ∈ closedBall (f x) (ε / 2 / 2)
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    ∀ y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
      ∀ y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I, ‖f y₁ - f y₂‖ ≤ ε / 2
have h : ∀ (δ : ℝ) (hδ : δ ∈ Set.Ioc 0 δ₁) (y₁ : Fin (n + 1) → ℝ)
  (hy₁ : y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) (y₂ : Fin (n + 1) → ℝ)
  (hy₂ : y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I), ‖f y₁ - f y₂‖ ≤ ε / 2
Tactic: filter_upwards [Ioc_mem_nhdsGT δ₁0] with δ hδ y₁ hy₁ y₂ hy₂
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ :
  ∀ x_1 ∈ closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
    f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
⊢ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ⊆
    closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
have h₁ : δ ≤ δ₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ :
  ∀ x_1 ∈ closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
    f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
⊢ ‖f y₁ - f y₂‖ ≤ ε / 2
have this : closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ⊆
  closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
Tactic: have : closedBall x δ ∩ (Box.Icc I) ⊆ closedBall x δ₁ ∩ (Box.Icc I) := by gcongr; exact hδ.2
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ :
  ∀ x_1 ∈ closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I,
    f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
this :
  closedBall x δ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ⊆
    closedBall x δ₁ ∩ (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I
⊢ ‖f y₁ - f y₂‖ ≤ ε / 2
have h : dist (f y₁) (f y₂) ≤ ε / 2
Tactic: rw [← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (2 * δ) ^ (n + 1) *
        norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) ≤
      ε / 2
have this : ContinuousWithinAt (Y := ℝ)
  (fun (δ : ℝ) ↦
    (2 * δ) ^ (n + 1) *
      norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
  (Set.Ioi 0) 0
Tactic: have : ContinuousWithinAt (fun δ : ℝ => (2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖)
            (Ioi 0) 0 := ((continuousWithinAt_id.const_mul _).pow _).mul_const _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
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
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x
ε : ℝ
ε0 : ε > 0
this :
  ContinuousWithinAt (Y := ℝ)
    (fun (δ : ℝ) ↦
      (2 * δ) ^ (n + 1) *
        norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
    (Set.Ioi 0) 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (2 * δ) ^ (n + 1) *
        norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) ≤
      ε / 2
have refine_2 : (fun (δ : ℝ) ↦
      (2 * δ) ^ (n + 1) *
        norm (E := E) ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
    0 <
  ε / 2
Tactic: refine this.eventually (ge_mem_nhds ?_)