ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → 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
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (splitCenterBox J s)
J' : Box ι
h' : J' ∈ splitCenter J
⊢ p J'
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → 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
refine' subbox_induction_on' I (fun J hle hs => H_ind J hle fun J' h' => _) H_nhds
case intro
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → 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
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (splitCenterBox J s)
s : Set ι
h' : splitCenterBox J s ∈ splitCenter J
⊢ p (splitCenterBox J s)
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → 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
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (splitCenterBox J s)
J' : Box ι
h' : J' ∈ splitCenter J
⊢ p J'
rcases mem_splitCenter.1 h' with ⟨s, rfl⟩
no goals
case intro
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → 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
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (splitCenterBox J s)
s : Set ι
h' : splitCenterBox J s ∈ splitCenter J
⊢ p (splitCenterBox J s)
exact hs s