-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem prepartition_isSubordinate (B : Box ι) {r : ℝ} (hr : 0 < r) (hn : 1 / n ≤ r) :
    (prepartition n B).IsSubordinate (fun _ ↦ ⟨r, hr⟩)

Proof state:
case intro.intro.refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ (prepartition n B).tag (box n ν) ∈ Box.Icc (box n ν)

Tactic:
rw [prepartition_tag n hν]

Result:
case intro.intro.refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ tag n ν ∈ Box.Icc (box n ν)

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
⊢ (prepartition n B).IsSubordinate fun x => ⟨r, hr⟩

Tactic:
intro _ hI

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
J✝ : Box ι
hI : J✝ ∈ prepartition n B
⊢ Box.Icc J✝ ⊆ Metric.closedBall ((prepartition n B).tag J✝) ↑((fun x => ⟨r, hr⟩) ((prepartition n B).tag J✝))

Proof state:
case intro.intro.refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ tag n ν ∈ Box.Icc (box n ν)

Tactic:
exact Box.coe_subset_Icc (tag_mem _ _)

Result:
no goals

Proof state:
case intro.intro.refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ Metric.diam (Box.Icc (box n ν)) ≤ ↑((fun x => ⟨r, hr⟩) ((prepartition n B).tag (box n ν)))

Tactic:
exact le_trans (diam_boxIcc n ν) hn

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ Box.Icc (box n ν) ⊆
    Metric.closedBall ((prepartition n B).tag (box n ν)) ↑((fun x => ⟨r, hr⟩) ((prepartition n B).tag (box n ν)))

Tactic:
refine fun _ h ↦ le_trans (Metric.dist_le_diam_of_mem (Box.isBounded_Icc _) h ?_) ?_

Result:
case intro.intro.refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ (prepartition n B).tag (box n ν) ∈ Box.Icc (box n ν)

case intro.intro.refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ Metric.diam (Box.Icc (box n ν)) ≤ ↑((fun x => ⟨r, hr⟩) ((prepartition n B).tag (box n ν)))

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
J✝ : Box ι
hI : J✝ ∈ prepartition n B
⊢ Box.Icc J✝ ⊆ Metric.closedBall ((prepartition n B).tag J✝) ↑((fun x => ⟨r, hr⟩) ((prepartition n B).tag J✝))

Tactic:
obtain ⟨ν, hν, rfl⟩ := mem_prepartition_iff.mp hI

Result:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ Box.Icc (box n ν) ⊆
    Metric.closedBall ((prepartition n B).tag (box n ν)) ↑((fun x => ⟨r, hr⟩) ((prepartition n B).tag (box n ν)))