awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J
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
⊢ False
have H_ind₁ : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬∀ (s : Set ι), p (J.splitCenterBox s)
Tactic: replace H_ind := fun J hJ ↦ not_imp_not.2 (H_ind J hJ)
Cleared hypotheses: H_ind
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
H_ind : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬∀ (s : Set ι), p (J.splitCenterBox s)
⊢ False
have H_ind₁ : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ∃ (x : Set ι), ¬p (J.splitCenterBox x)
Tactic: simp only [not_forall] at H_ind
Cleared hypotheses: H_ind
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
H_ind : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ∃ (x : Set ι), ¬p (J.splitCenterBox x)
⊢ False
have choose! : ∀ (s : (J : Box ι) → Set ι) (hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))), False
Tactic: choose! s hs using H_ind
Cleared hypotheses: H_ind
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
Tactic: have J_succ : ∀ m, J (m + 1) = splitCenterBox (J m) (s <| J m) :=
    fun m ↦ iterate_succ_apply' _ _ _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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))
⊢ False
have hJmono : Antitone J
Tactic: have hJmono : Antitone J :=
    antitone_nat_of_succ_le fun n ↦ by simpa [J_succ] using splitCenterBox_le _ _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have hJle : ∀ (m : ℕ), J m ≤ I
Tactic: have hJle (m) : J m ≤ I := hJmono zero_le
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have hJp : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
have zero : (J 0).upper i - (J 0).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) (β := ℕ) 2 0
Tactic: induction m with
    | zero => simp [J]
    | succ m ihm => simp only [pow_succ, J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
⊢ (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m
have 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)
Tactic: induction m with
    | zero => simp [J]
    | succ m ihm => simp only [pow_succ, J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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)
⊢ False
have hJsub : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have h0 : J 0 = I
Tactic: have h0 : J 0 = I := rfl
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
⊢ False
have 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
Tactic: clear_value J
Cleared hypotheses: J, J_succ, hJmono, hJle, hJp, hJsub, h0
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have hzJ : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have hJl_mem : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have hJu_mem : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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
⊢ False
have hJlz : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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)
have suffices : Tendsto.{0, u_1} (β := ι → ℝ) (fun (m : ℕ) ↦ (J m).upper - (J m).lower) atTop (𝓝 0)
Tactic: suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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)
have refine : ∀ (i : ι), Tendsto (β := ℝ) (fun (i_1 : ℕ) ↦ ((J i_1).upper - (J i_1).lower) i) atTop (𝓝 (0 i))
Tactic: refine tendsto_pi_nhds.2 fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (hypothesis)
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)
⊢ False
have hJuz : 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)