case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ distortion (Prepartition.biUnionTagged π πi) ≤ c

case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi) ∧
      Prepartition.distortion π' ≤ c
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
⊢ MemBaseSet l I c r (Prepartition.biUnionTagged π πi)
refine' ⟨TaggedPrepartition.isSubordinate_biUnionTagged.2 fun J hJ => (h J hJ).1,
  fun hH => TaggedPrepartition.isHenstock_biUnionTagged.2 fun J hJ => (h J hJ).2 hH,
  fun hD => _, fun hD => _⟩
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∀ (b : Box ι), b ∈ π.boxes → distortion (πi b) ≤ c
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ distortion (Prepartition.biUnionTagged π πi) ≤ c
rw [Prepartition.distortion_biUnionTagged, Finset.sup_le_iff]
no goals
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∀ (b : Box ι), b ∈ π.boxes → distortion (πi b) ≤ c
exact fun J hJ => (h J hJ).3 hD
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ Prepartition.iUnion (Prepartition.compl π) = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi) ∧
      Prepartition.distortion π' ≤ c
refine' ⟨_, _, hc hD⟩
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ↑I \ Prepartition.iUnion (Prepartition.biUnion π fun J => (πi J).toPrepartition) =
    ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ Prepartition.iUnion (Prepartition.compl π) = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]
no goals
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ↑I \ Prepartition.iUnion (Prepartition.biUnion π fun J => (πi J).toPrepartition) =
    ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
rfl