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
I : Box ι
l : IntegrationParams
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ toFilteriUnion l I π₁ = toFilteriUnion l I π₂
simp only [toFilteriUnion, toFilterDistortioniUnion, h]