no goals
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ₁ : MemBaseSet l I c r₁ π₁
hle : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → r₂ x ≤ r₁ x
π₂ : Prepartition I
hU : Prepartition.iUnion π₂ = ↑I \ TaggedPrepartition.iUnion π₁
hc : l.bDistortion = true → Prepartition.distortion π₂ ≤ c
x✝ : l.bDistortion = true
⊢ Prepartition.iUnion ⊥ = ↑I \ TaggedPrepartition.iUnion (unionComplToSubordinate π₁ π₂ hU r₂) ∧
    Prepartition.distortion ⊥ ≤ c
simp