case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))

case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
⊢ IsSubordinate (TaggedPrepartition.disjUnion π₁ π₂ h) r
refine' fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => _) fun hJ => _
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₁ J) ↑(r (tag π₁ J))
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))
rw [disjUnion_tag_of_mem_left _ hJ]
no goals
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₁ J) ↑(r (tag π₁ J))
exact h₁ _ hJ
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₂ J) ↑(r (tag π₂ J))
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))
rw [disjUnion_tag_of_mem_right _ hJ]
no goals
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₂ J) ↑(r (tag π₂ J))
exact h₂ _ hJ