case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h✝ : IsPartition π
hx✝ : x ∈ I
J : Box ι
h : J ∈ π
hx : x ∈ J
⊢ ∃! J x_1, x ∈ J
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : IsPartition π
hx : x ∈ I
⊢ ∃! J x_1, x ∈ J
rcases h x hx with ⟨J, h, hx⟩
no goals
case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h✝ : IsPartition π
hx✝ : x ∈ I
J : Box ι
h : J ∈ π
hx : x ∈ J
⊢ ∃! J x_1, x ∈ J
exact ExistsUnique.intro₂ J h hx fun J' h' hx' => π.eq_of_mem_of_mem h' h hx' hx