awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝 z)
i : ι
⊢ Tendsto (β := ℝ) (fun (i_1 : ℕ) ↦ ((J i_1).upper - (J i_1).lower) i) atTop (𝓝 (0 i))

Tactic:
simpa [hJsub] using
      tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)

Premises used: Filter.Tendsto.div_atTop, tendsto_const_nhds, tendsto_pow_atTop_atTop_of_one_lt, one_lt_two
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝 z)
⊢ Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝 z)

Tactic:
have hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z) := by
    suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
    refine tendsto_pi_nhds.2 fun i ↦ ?_
    simpa [hJsub] using
      tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝 z)
hJuz : Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝 z)
⊢ Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)

Tactic:
replace hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z) :=
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (Eventually.of_forall hJl_mem)
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJuz : Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝 z)
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
⊢ Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)

Tactic:
replace hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z) :=
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJuz (Eventually.of_forall hJu_mem)
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
hJuz : Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
rcases :
  ∀ (U : Set (ι → ℝ)) (hUz : U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z)
    (hU :
      ∀ J ≤ I,
        ∀ (m : ℕ),
          Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
              (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J),
    False
⊢ False

Tactic:
rcases H_nhds z (h0 ▸ hzJ 0) with ⟨U, hUz, hU⟩

Premises used: Eq.rec, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
hJuz : Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z
hU :
  ∀ J ≤ I,
    ∀ (m : ℕ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
        (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
          (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
rcases : ∀ (m : ℕ) (hUm : Icc (J m).lower (J m).upper ∈ 𝒫 U), False
⊢ False

Tactic:
rcases (tendsto_lift'.1 (hJlz.Icc hJuz) U hUz).exists with ⟨m, hUm⟩

Premises used: Filter.tendsto_lift', Filter.Tendsto.Icc, Filter.Eventually.exists, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
hJuz : Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z
hU :
  ∀ J ≤ I,
    ∀ (m : ℕ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
        (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
          (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
m : ℕ
hUm : Icc (J m).lower (J m).upper ∈ 𝒫 U
⊢ False

Tactic:
hJp m (hU (J m) (hJle m) m (hzJ m) hUm (hJsub m))
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z
hJl_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower
hJu_mem :
  ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper
hJlz : Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
hJuz : Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z
hU :
  ∀ J ≤ I,
    ∀ (m : ℕ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
        (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
          (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
m : ℕ
hUm : Icc (J m).lower (J m).upper ∈ 𝒫 U
⊢ False

Tactic:
exact hJp m (hU (J m) (hJle m) m (hzJ m) hUm (hJsub m))
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
set :
  let e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ);
  ‖HSMul.hSMul (α := ℝ) (β := E) (∏ j : Fin (n + 1), (I.upper j - I.lower j))
          ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * (↑c : ℝ) * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
⊢ ‖HSMul.hSMul (α := ℝ) (β := E) (∏ j : Fin (n + 1), (I.upper j - I.lower j))
          ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) -
        (integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * (↑c : ℝ) * ∏ j : Fin (n + 1), (I.upper j - I.lower j)

Tactic:
set e : ℝ → (Fin n → ℝ) → (Fin (n + 1) → ℝ) := i.insertNth (α := fun _ ↦ ℝ)

Premises used: Fin.insertNth
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
⊢ I.lower i ∈ Set.Icc (I.lower i) (I.upper i)

Tactic:
have Hl : I.lower i ∈ Icc (I.lower i) (I.upper i) := Set.left_mem_Icc.2 (I.lower_le_upper i)
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
⊢ I.upper i ∈ Set.Icc (I.lower i) (I.upper i)

Tactic:
have Hu : I.upper i ∈ Icc (I.lower i) (I.upper i) := Set.right_mem_Icc.2 (I.lower_le_upper i)
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
⊢ ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume

Tactic:
have Hi : ∀ x ∈ Icc (I.lower i) (I.upper i),
      Integrable.{0, u, u} (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume := fun x hx =>
    integrable_of_continuousOn _ (Box.continuousOn_face_Icc hfc hx) volume
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy :
  Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ)) y
⊢ let g : (y : Fin (n + 1) → ℝ) → E := fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E);
  g = fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)

Tactic:
set g := fun y => f y - a - f' (y - x) with hg

Premises used: HSub.hSub, DFunLike.coe
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy :
  Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ)) y
g : (y : Fin (n + 1) → ℝ) → E :=
  fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
hg : g = fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
⊢ ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖g y‖ ≤ ε * ‖y - x‖

Tactic:
change ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * ‖y - x‖ at hε

Premises used: BoxIntegral.Box.Icc, DFunLike.coe