From 1ec0483fe11f133344b04436cc01bcf71b3b9cb3 Mon Sep 17 00:00:00 2001 From: euprunin Date: Tue, 25 Nov 2025 20:01:24 +0100 Subject: [PATCH] chore(MeasureTheory/MeasurableSpace): golf `generateFrom_pi_eq` using `grind` --- Mathlib/MeasureTheory/MeasurableSpace/Pi.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean b/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean index 9ac1896f535108..b0bc3d707c2ad1 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean @@ -84,10 +84,8 @@ theorem generateFrom_pi_eq {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountabl rw [this, ← iUnion_univ_pi] apply MeasurableSet.iUnion intro n; apply measurableSet_generateFrom - apply mem_image_of_mem; intro j _; dsimp only - by_cases h : j = i - · subst h; rwa [update_self] - · rw [update_of_ne h]; apply h1t + apply mem_image_of_mem + grind · apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩ rw [univ_pi_eq_iInter]; apply MeasurableSet.iInter; intro i apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))