-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_admissibleIndex_of_mem_box {B : Box ι} (hB : hasIntegralVertices B) {x : ι → ℝ}
    (hx : x ∈ B) : index n x ∈ admissibleIndex n B

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ index n x ∈ admissibleIndex n B

Tactic:
obtain ⟨l, u, hl, hu⟩ := hB

Result:
case intro.intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ index n x ∈ admissibleIndex n B

Proof state:
case intro.intro.intro.refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
i : ι
⊢ ↑(l i) ≤ (↑⌈↑n * x i⌉ - 1) / ↑n

Tactic:
exact (mem_admissibleIndex_of_mem_box_aux₁ n (x i) (l i)).mp ((hl i) ▸ (hx i).1)

Result:
no goals

Proof state:
case intro.intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ ∀ (x_1 : ι), ↑(l x_1) ≤ ↑(⌈↑n * x x_1⌉ - 1) / ↑n ∧ (↑(⌈↑n * x x_1⌉ - 1) + 1) / ↑n ≤ ↑(u x_1)

Tactic:
push_cast

Result:
case intro.intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ ∀ (x_1 : ι), ↑(l x_1) ≤ (↑⌈↑n * x x_1⌉ - 1) / ↑n ∧ (↑⌈↑n * x x_1⌉ - 1 + 1) / ↑n ≤ ↑(u x_1)

Proof state:
case intro.intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ index n x ∈ admissibleIndex n B

Tactic:
simp_rw [mem_admissibleIndex_iff, Box.le_iff_bounds, box_lower, box_upper, Pi.le_def,
  index_apply, hl, hu, ← forall_and]

Result:
case intro.intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ ∀ (x_1 : ι), ↑(l x_1) ≤ ↑(⌈↑n * x x_1⌉ - 1) / ↑n ∧ (↑(⌈↑n * x x_1⌉ - 1) + 1) / ↑n ≤ ↑(u x_1)

Proof state:
case intro.intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ ∀ (x_1 : ι), ↑(l x_1) ≤ (↑⌈↑n * x x_1⌉ - 1) / ↑n ∧ (↑⌈↑n * x x_1⌉ - 1 + 1) / ↑n ≤ ↑(u x_1)

Tactic:
refine fun i ↦ ⟨?_, ?_⟩

Result:
case intro.intro.intro.refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
i : ι
⊢ ↑(l i) ≤ (↑⌈↑n * x i⌉ - 1) / ↑n

case intro.intro.intro.refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
i : ι
⊢ (↑⌈↑n * x i⌉ - 1 + 1) / ↑n ≤ ↑(u i)

Proof state:
case intro.intro.intro.refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
i : ι
⊢ (↑⌈↑n * x i⌉ - 1 + 1) / ↑n ≤ ↑(u i)

Tactic:
exact (mem_admissibleIndex_of_mem_box_aux₂ n (x i) (u i)).mp ((hu i) ▸ (hx i).2)

Result:
no goals