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

case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag (TaggedPrepartition.disjUnion π₁ π₂ h) J ∈ ↑Box.Icc J
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
⊢ IsHenstock (TaggedPrepartition.disjUnion π₁ π₂ h)
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)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ tag π₁ J ∈ ↑Box.Icc J
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ tag (TaggedPrepartition.disjUnion π₁ π₂ h) J ∈ ↑Box.Icc 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)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ tag π₁ J ∈ ↑Box.Icc J
exact h₁ _ hJ
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag π₂ J ∈ ↑Box.Icc J
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag (TaggedPrepartition.disjUnion π₁ π₂ h) J ∈ ↑Box.Icc 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)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag π₂ J ∈ ↑Box.Icc J
exact h₂ _ hJ