From 4f3c460cc1668820c9af8418a87a23db44c7acab Mon Sep 17 00:00:00 2001 From: JovanGerb Date: Sat, 18 May 2024 06:53:34 +0000 Subject: [PATCH] . --- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean index da2e61956cb17..81d778db5570e 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean @@ -622,7 +622,7 @@ theorem filter_true : (π.filter fun _ => True) = π := theorem iUnion_filter_not (π : Prepartition I) (p : Box ι → Prop) : (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion := by simp only [Prepartition.iUnion] - convert (@Set.biUnion_diff_biUnion_eq _ (Box ι) π.boxes (π.filter p).boxes Box.toSet _).symm + convert (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm · simp (config := { contextual := true }) · rw [Set.PairwiseDisjoint] convert π.pairwiseDisjoint