[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i <
    Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i
[PROOFSTEP]
dsimp only [Set.piecewise]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ (if i ∈ s then (lower I i + upper I i) / 2 else lower I i) < if i ∈ s then upper I i else (lower I i + upper I i) / 2
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ (lower I i + upper I i) / 2 < upper I i
[PROOFSTEP]
simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]
[GOAL]
case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : ¬i ∈ s
⊢ lower I i < (lower I i + upper I i) / 2
[PROOFSTEP]
simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
⊢ y ∈ splitCenterBox I s ↔ y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ s
[PROOFSTEP]
simp only [splitCenterBox, mem_def, ← forall_and]
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
⊢ (∀ (i : ι),
      y i ∈
        Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
          (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Set.Ioc (lower I x) (upper I x) ∧ ((lower I x + upper I x) / 2 < y x ↔ x ∈ s)
[PROOFSTEP]
refine' forall_congr' fun i ↦ _
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
        (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
dsimp only [Set.piecewise]
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (if i ∈ s then (lower I i + upper I i) / 2 else lower I i)
        (if i ∈ s then upper I i else (lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
split_ifs with hs
[GOAL]
case pos
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Set.Ioc ((lower I i + upper I i) / 2) (upper I i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
simp only [hs, iff_true_iff, iff_false_iff, not_lt]
[GOAL]
case neg
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : ¬i ∈ s
⊢ y i ∈ Set.Ioc (lower I i) ((lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
simp only [hs, iff_true_iff, iff_false_iff, not_lt]
[GOAL]
case pos
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Set.Ioc ((lower I i + upper I i) / 2) (upper I i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ (lower I i + upper I i) / 2 < y i
case neg
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : ¬i ∈ s
⊢ y i ∈ Set.Ioc (lower I i) ((lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ y i ≤ (lower I i + upper I i) / 2
[PROOFSTEP]
exacts [⟨fun H ↦ ⟨⟨(left_lt_add_div_two.2 (I.lower_lt_upper i)).trans H.1, H.2⟩, H.1⟩, fun H ↦ ⟨H.2, H.1.2⟩⟩,
  ⟨fun H ↦ ⟨⟨H.1, H.2.trans (add_div_two_lt_right.2 (I.lower_lt_upper i)).le⟩, H.2⟩, fun H ↦ ⟨H.1.1, H.2⟩⟩]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
⊢ Disjoint ↑(splitCenterBox I s) ↑(splitCenterBox I t)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(splitCenterBox I s) ⊓ ↑(splitCenterBox I t) ≤ ⊥
[PROOFSTEP]
rintro y ⟨hs, ht⟩
[GOAL]
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ y ∈ ⊥
[PROOFSTEP]
apply h
[GOAL]
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ s = t
[PROOFSTEP]
ext i
[GOAL]
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
i : ι
⊢ i ∈ s ↔ i ∈ t
[PROOFSTEP]
rw [mem_coe, mem_splitCenterBox] at hs ht 
[GOAL]
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ t
i : ι
⊢ i ∈ s ↔ i ∈ t
[PROOFSTEP]
rw [← hs.2, ← ht.2]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
⊢ ⋃ (s : Set ι), ↑(splitCenterBox I s) = ↑I
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
I✝ J I : Box ι
x : ι → ℝ
⊢ x ∈ ⋃ (s : Set ι), ↑(splitCenterBox I s) ↔ x ∈ ↑I
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
by_cases i ∈ s
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
by_cases i ∈ s
[GOAL]
case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : i ∈ s
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
field_simp [splitCenterBox]
[GOAL]
case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : ¬i ∈ s
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
field_simp [splitCenterBox]
[GOAL]
case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : i ∈ s
⊢ upper I i * 2 - (lower I i + upper I i) = upper I i - lower I i
[PROOFSTEP]
field_simp [mul_two, two_mul]
[GOAL]
case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : ¬i ∈ s
⊢ lower I i + upper I i - 2 * lower I i = upper I i - lower I i
[PROOFSTEP]
field_simp [mul_two, two_mul]
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (s : Set ι), p (splitCenterBox J s)) → p J
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
⊢ p I
[PROOFSTEP]
by_contra hpI
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (s : Set ι), p (splitCenterBox J s)) → p J
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
⊢ False
[PROOFSTEP]
replace H_ind := fun J hJ ↦ not_imp_not.2 (H_ind J hJ)
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
H_ind : ∀ (J : Box ι), J ≤ I → ¬p J → ¬∀ (s : Set ι), p (splitCenterBox J s)
⊢ False
[PROOFSTEP]
simp only [exists_imp, not_forall] at H_ind 
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
H_ind : ∀ (J : Box ι), J ≤ I → ¬p J → ∃ x, ¬p (splitCenterBox J x)
⊢ False
[PROOFSTEP]
choose! s hs using H_ind
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
⊢ False
[PROOFSTEP]
set J : ℕ → Box ι := fun m ↦ (fun J ↦ splitCenterBox J (s J))^[m] I
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
⊢ False
[PROOFSTEP]
have J_succ : ∀ m, J (m + 1) = splitCenterBox (J m) (s <| J m) := fun m ↦
  iterate_succ_apply' _ _
    _
      -- Now we prove some properties of `J`
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
⊢ False
[PROOFSTEP]
have hJmono : Antitone J := antitone_nat_of_succ_le fun n ↦ by simpa [J_succ] using splitCenterBox_le _ _
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
n : ℕ
⊢ J (n + 1) ≤ J n
[PROOFSTEP]
simpa [J_succ] using splitCenterBox_le _ _
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
⊢ False
[PROOFSTEP]
have hJle : ∀ m, J m ≤ I := fun m ↦ hJmono (zero_le m)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
⊢ False
[PROOFSTEP]
have hJp : ∀ m, ¬p (J m) := fun m ↦ Nat.recOn m hpI fun m ↦ by simpa only [J_succ] using hs (J m) (hJle m)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
m✝ m : ℕ
⊢ ¬p (J m) → ¬p (J (Nat.succ m))
[PROOFSTEP]
simpa only [J_succ] using hs (J m) (hJle m)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
⊢ False
[PROOFSTEP]
have hJsub : ∀ m i, (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m :=
  by
  intro m i
  induction' m with m ihm
  · simp [Nat.zero_eq]
  simp only [pow_succ', J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
⊢ ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
[PROOFSTEP]
intro m i
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
m : ℕ
i : ι
⊢ upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
[PROOFSTEP]
induction' m with m ihm
[GOAL]
case zero
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
⊢ upper (J Nat.zero) i - lower (J Nat.zero) i = (upper I i - lower I i) / 2 ^ Nat.zero
[PROOFSTEP]
simp [Nat.zero_eq]
[GOAL]
case succ
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
m : ℕ
ihm : upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
⊢ upper (J (Nat.succ m)) i - lower (J (Nat.succ m)) i = (upper I i - lower I i) / 2 ^ Nat.succ m
[PROOFSTEP]
simp only [pow_succ', J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
⊢ False
[PROOFSTEP]
have h0 : J 0 = I := rfl
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
⊢ False
[PROOFSTEP]
clear_value J
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
⊢ False
[PROOFSTEP]
clear hpI hs J_succ s
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
⊢ False
[PROOFSTEP]
set z : ι → ℝ := ⨆ m, (J m).lower
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
⊢ False
[PROOFSTEP]
have hzJ : ∀ m, z ∈ Box.Icc (J m) :=
  mem_iInter.1
    (ciSup_mem_Inter_Icc_of_antitone_Icc ((@Box.Icc ι).monotone.comp_antitone hJmono) fun m ↦ (J m).lower_le_upper)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
⊢ False
[PROOFSTEP]
have hJl_mem : ∀ m, (J m).lower ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).lower_mem_Icc
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
⊢ False
[PROOFSTEP]
have hJu_mem : ∀ m, (J m).upper ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).upper_mem_Icc
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
⊢ False
[PROOFSTEP]
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⟩
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
⊢ False
[PROOFSTEP]
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)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
⊢ Tendsto (fun m => (J m).upper) atTop (𝓝 z)
[PROOFSTEP]
suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
this : Tendsto (fun m => (J m).upper - (J m).lower) atTop (𝓝 0)
⊢ Tendsto (fun m => (J m).upper) atTop (𝓝 z)
[PROOFSTEP]
simpa using hJlz.add this
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
⊢ Tendsto (fun m => (J m).upper - (J m).lower) atTop (𝓝 0)
[PROOFSTEP]
refine' tendsto_pi_nhds.2 fun i ↦ _
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
i : ι
⊢ Tendsto (fun i_1 => ((J i_1).upper - (J i_1).lower) i) atTop (𝓝 (OfNat.ofNat 0 i))
[PROOFSTEP]
simpa [hJsub] using tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)
⊢ False
[PROOFSTEP]
replace hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
[GOAL]
case hJlz
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
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 (𝓝[Set.Icc I.lower I.upper] z)
[PROOFSTEP]
exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (eventually_of_forall hJl_mem)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
⊢ False
[PROOFSTEP]
replace hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
[GOAL]
case hJuz
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
⊢ Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
[PROOFSTEP]
exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJuz (eventually_of_forall hJu_mem)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
⊢ False
[PROOFSTEP]
rcases H_nhds z (h0 ▸ hzJ 0) with ⟨U, hUz, hU⟩
[GOAL]
case intro.intro
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[↑Box.Icc I] z
hU :
  ∀ (J : Box ι),
    J ≤ I →
      ∀ (m : ℕ),
        z ∈ ↑Box.Icc J → ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
⊢ False
[PROOFSTEP]
rcases(tendsto_lift'.1 (hJlz.Icc hJuz) U hUz).exists with ⟨m, hUm⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[↑Box.Icc I] z
hU :
  ∀ (J : Box ι),
    J ≤ I →
      ∀ (m : ℕ),
        z ∈ ↑Box.Icc J → ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
m : ℕ
hUm : Set.Icc (J m).lower (J m).upper ∈ 𝒫 U
⊢ False
[PROOFSTEP]
exact hJp m (hU (J m) (hJle m) m (hzJ m) hUm (hJsub m))
