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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
n : ℕ
⊢ J (n + 1) ≤ J n

Tactic:
simpa [J_succ] using splitCenterBox_le _ _

Premises used: BoxIntegral.Box.splitCenterBox_le
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
⊢ Antitone J

Tactic:
have hJmono : Antitone J :=
    antitone_nat_of_succ_le fun n ↦ by simpa [J_succ] using splitCenterBox_le _ _
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
⊢ ∀ (m : ℕ), J m ≤ I

Tactic:
have hJle (m) : J m ≤ I := hJmono zero_le
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
m_1 m : ℕ
⊢ ∀ (n_ih : ¬p (J m)), ¬p (J m.succ)

Tactic:
simpa only [J_succ] using hs (J m) (hJle 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
⊢ ∀ (m : ℕ), ¬p (J m)

Tactic:
have hJp (m) : ¬p (J m) := Nat.recOn m hpI fun m ↦ by simpa only [J_succ] using hs (J m) (hJle 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
⊢ (J 0).upper i - (J 0).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) (β := ℕ) 2 0

Tactic:
simp [J]
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
m : ℕ
ihm : (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
⊢ (J (m + 1)).upper i - (J (m + 1)).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 (m + 1)

Tactic:
simp only [pow_succ, J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]

Premises used: BoxIntegral.Box.upper_sub_lower_splitCenterBox, pow_succ, div_div
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
m : ℕ
i : ι
zero : (J 0).upper i - (J 0).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) (β := ℕ) 2 0
succ :
  ∀ (m : ℕ) (ihm : (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m),
    (J (m + 1)).upper i - (J (m + 1)).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 (m + 1)
⊢ (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m

Tactic:
induction m with
    | zero => simp [J]
    | succ m ihm => simp only [pow_succ, J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]

Premises used: BoxIntegral.Box.upper_sub_lower_splitCenterBox, pow_succ, div_div
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
⊢ ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m

Tactic:
have hJsub (m i) : (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m := by
    induction m with
    | zero => simp [J]
    | succ m ihm => simp only [pow_succ, J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
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
⊢ J 0 = I

Tactic:
have h0 : J 0 = I := rfl
-- 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
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
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
clear_value :
  ∀ (J : ℕ → Box ι) (J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))) (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), False
⊢ False

Tactic:
clear_value J
-- 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
⊢ ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (J m) : Set (ι → ℝ)) z

Tactic:
have hzJ : ∀ m, z ∈ Box.Icc (J m) :=
    mem_iInter.1 (ciSup_mem_iInter_Icc_of_antitone_Icc
      ((@Box.Icc ι).monotone.comp_antitone hJmono) fun m ↦ (J m).lower_le_upper)
-- 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
⊢ ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).lower

Tactic:
have hJl_mem : ∀ m, (J m).lower ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).lower_mem_Icc
-- 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
⊢ ∀ (m : ℕ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (J m).upper

Tactic:
have hJu_mem : ∀ m, (J m).upper ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).upper_mem_Icc
-- 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
⊢ Tendsto (fun (m : ℕ) ↦ (J m).lower) atTop (𝓝 z)

Tactic:
have hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z) :=
    tendsto_atTop_ciSup (antitone_lower.comp hJmono) ⟨I.upper, fun x ⟨m, hm⟩ ↦ hm ▸ (hJl_mem m).2⟩
-- 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)
this : Tendsto.{0, u_1} (β := ι → ℝ) (fun (m : ℕ) ↦ (J m).upper - (J m).lower) atTop (𝓝 0)
⊢ Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝 z)

Tactic:
simpa using hJlz.add this

Premises used: Filter.Tendsto.add
-- 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)
suffices : Tendsto.{0, u_1} (β := ι → ℝ) (fun (m : ℕ) ↦ (J m).upper - (J m).lower) atTop (𝓝 0)
⊢ Tendsto (fun (m : ℕ) ↦ (J m).upper) atTop (𝓝 z)

Tactic:
suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
-- 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.{0, u_1} (β := ι → ℝ) (fun (m : ℕ) ↦ (J m).upper - (J m).lower) atTop (𝓝 0)

Tactic:
tendsto_pi_nhds.2 fun i ↦ ?_

Premises used: Iff.mpr, tendsto_pi_nhds
-- 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)
refine : ∀ (i : ι), Tendsto (β := ℝ) (fun (i_1 : ℕ) ↦ ((J i_1).upper - (J i_1).lower) i) atTop (𝓝 (0 i))
⊢ Tendsto.{0, u_1} (β := ι → ℝ) (fun (m : ℕ) ↦ (J m).upper - (J m).lower) atTop (𝓝 0)

Tactic:
refine tendsto_pi_nhds.2 fun i ↦ ?_

Premises used: Iff.mpr, tendsto_pi_nhds