-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem BoxIntegral.le_hasIntegralVertices_of_isBounded [Finite ι] {s : Set (ι → ℝ)}
    (h : IsBounded s) :
    ∃ B : BoxIntegral.Box ι, hasIntegralVertices B ∧ s ≤ B

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
⊢ Metric.ball 0 ↑C ≤ ↑I

Tactic:
intro x hx

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : x ∈ Metric.ball 0 ↑C
⊢ x ∈ ↑I

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Tactic:
let I : Box ι := Box.mk (fun _ ↦ - C) (fun _ ↦ C )
  (fun _ ↦ by simp [C, neg_lt_self_iff, Nat.cast_pos, hC])

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Proof state:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
x✝ : ι
⊢ (fun x => -↑C) x✝ < (fun x => ↑C) x✝

Tactic:
simp [C, neg_lt_self_iff, Nat.cast_pos, hC]

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
⊢ Metric.ball 0 R ≤ ↑I

Tactic:
suffices Metric.ball (0 : ι → ℝ) C ≤ I from
  le_trans (Metric.ball_subset_ball (Nat.le_ceil R)) this

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
⊢ Metric.ball 0 ↑C ≤ ↑I

Proof state:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Tactic:
obtain ⟨R, hR₁, hR₂⟩ := IsBounded.subset_ball_lt h 0 0

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Tactic:
refine ⟨I, ⟨fun _ ↦ - C, fun _ ↦ C, fun i ↦ (Int.cast_neg_natCast C).symm, fun _ ↦ rfl⟩,
  le_trans hR₂ ?_⟩

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
⊢ Metric.ball 0 R ≤ ↑I

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Tactic:
let C : ℕ := ⌈R⌉₊

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : x ∈ Metric.ball 0 ↑C
⊢ x ∈ ↑I

Tactic:
simp_rw [C, mem_ball_zero_iff, pi_norm_lt_iff (Nat.cast_pos.mpr hC),
  Real.norm_eq_abs, abs_lt] at hx

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : ∀ (i : ι), -↑⌈R⌉₊ < x i ∧ x i < ↑⌈R⌉₊
⊢ x ∈ ↑I

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Tactic:
have hC := Nat.ceil_pos.mpr hR₁

Result:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Proof state:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Tactic:
have := Fintype.ofFinite ι

Result:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
⊢ ∃ B, hasIntegralVertices B ∧ s ≤ ↑B

Proof state:
case intro.intro
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x => -↑C, upper := fun x => ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : ∀ (i : ι), -↑⌈R⌉₊ < x i ∧ x i < ↑⌈R⌉₊
⊢ x ∈ ↑I

Tactic:
exact fun i ↦ ⟨(hx i).1, le_of_lt (hx i).2⟩

Result:
no goals