chore(MeasureTheory/MeasurableSpace): golf generateFrom_pi_eq using grind

[euprunin]

---

Show trace profiling of generateFrom_pi_eq: 60 ms before, 60 ms after 🎉

Trace profiling of generateFrom_pi_eq before PR 32112

diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean b/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
index 9ac1896f53..fc5859a2c5 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
@@ -61,6 +61,7 @@ theorem IsCountablySpanning.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCoun
     [e, (surjective_decode_iget (ι → ℕ)).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
     iUnion_univ_pi s, h2s, pi_univ]
 
+set_option trace.profiler true in
 /-- The product of generated σ-algebras is the one generated by boxes, if both generating sets
   are countably spanning. -/
 theorem generateFrom_pi_eq {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :

ℹ [847/847] Built Mathlib.MeasureTheory.MeasurableSpace.Pi (1.0s)
info: Mathlib/MeasureTheory/MeasurableSpace/Pi.lean:65:0: [Elab.async] [0.062051] elaborating proof of generateFrom_pi_eq
  [Elab.definition.value] [0.060427] generateFrom_pi_eq
    [Elab.step] [0.058095] classical
          cases nonempty_encodable ι
          apply le_antisymm
          · refine iSup_le ?_; intro i; rw [comap_generateFrom]
            apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
            choose t h1t h2t using hC
            simp_rw [eval_preimage, ← h2t]
            rw [← @iUnion_const _ ℕ _ s]
            have :
              Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
              by
              ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
              by_cases h : i' = i
              · subst h; simp
              · simp [h]
            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 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))
            exact measurableSet_generateFrom (hs i (mem_univ i))
      [Elab.step] [0.058089] classical
            cases nonempty_encodable ι
            apply le_antisymm
            · refine iSup_le ?_; intro i; rw [comap_generateFrom]
              apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
              choose t h1t h2t using hC
              simp_rw [eval_preimage, ← h2t]
              rw [← @iUnion_const _ ℕ _ s]
              have :
                Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                  Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                by
                ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                by_cases h : i' = i
                · subst h; simp
                · simp [h]
              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 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))
              exact measurableSet_generateFrom (hs i (mem_univ i))
        [Elab.step] [0.058084] classical
            cases nonempty_encodable ι
            apply le_antisymm
            · refine iSup_le ?_; intro i; rw [comap_generateFrom]
              apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
              choose t h1t h2t using hC
              simp_rw [eval_preimage, ← h2t]
              rw [← @iUnion_const _ ℕ _ s]
              have :
                Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                  Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                by
                ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                by_cases h : i' = i
                · subst h; simp
                · simp [h]
              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 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))
              exact measurableSet_generateFrom (hs i (mem_univ i))
          [Elab.step] [0.057931] 
                cases nonempty_encodable ι
                apply le_antisymm
                · refine iSup_le ?_; intro i; rw [comap_generateFrom]
                  apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
                  choose t h1t h2t using hC
                  simp_rw [eval_preimage, ← h2t]
                  rw [← @iUnion_const _ ℕ _ s]
                  have :
                    Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                      Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                    by
                    ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                    by_cases h : i' = i
                    · subst h; simp
                    · simp [h]
[… 92 lines omitted …]
                          · subst h; simp
                          · simp [h]
                        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
                    [Elab.step] [0.017084] simp_rw [eval_preimage, ← h2t]
                    [Elab.step] [0.018496] have :
                          Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                            Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                          by
                          ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                          by_cases h : i' = i
                          · subst h; simp
                          · simp [h]
                      [Elab.step] [0.018479] focus
                            refine
                              no_implicit_lambda%
                                (have :
                                  Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                                    Set.pi univ fun k =>
                                      ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                                  ?body✝;
                                ?_)
                            case body✝ =>
                              with_annotate_state"by"
                                ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                  by_cases h : i' = i
                                  · subst h; simp
                                  · simp [h])
                        [Elab.step] [0.018475] 
                              refine
                                no_implicit_lambda%
                                  (have :
                                    Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                                      Set.pi univ fun k =>
                                        ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                                    ?body✝;
                                  ?_)
                              case body✝ =>
                                with_annotate_state"by"
                                  ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                    by_cases h : i' = i
                                    · subst h; simp
                                    · simp [h])
                          [Elab.step] [0.018473] 
                                refine
                                  no_implicit_lambda%
                                    (have :
                                      Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                                        Set.pi univ fun k =>
                                          ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                                      ?body✝;
                                    ?_)
                                case body✝ =>
                                  with_annotate_state"by"
                                    ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                      by_cases h : i' = i
                                      · subst h; simp
                                      · simp [h])
                            [Elab.step] [0.014848] case body✝ =>
                                  with_annotate_state"by"
                                    ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                      by_cases h : i' = i
                                      · subst h; simp
                                      · simp [h])
                              [Elab.step] [0.014811] with_annotate_state"by"
                                      ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                        by_cases h : i' = i
                                        · subst h; simp
                                        · simp [h])
                                [Elab.step] [0.014808] with_annotate_state"by"
                                        ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                          by_cases h : i' = i
                                          · subst h; simp
                                          · simp [h])
                                  [Elab.step] [0.014806] with_annotate_state"by"
                                        ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                          by_cases h : i' = i
                                          · subst h; simp
                                          · simp [h])
                                    [Elab.step] [0.014803] (
                                          ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                          by_cases h : i' = i
                                          · subst h; simp
                                          · simp [h])
                                      [Elab.step] [0.014801] 
                                            ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                            by_cases h : i' = i
                                            · subst h; simp
                                            · simp [h]
                                        [Elab.step] [0.014797] 
                                              ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                              by_cases h : i' = i
                                              · subst h; simp
                                              · simp [h]
Build completed successfully (847 jobs).

Trace profiling of generateFrom_pi_eq after PR 32112

diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean b/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
index 9ac1896f53..26e37c73b9 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
@@ -61,6 +61,7 @@ theorem IsCountablySpanning.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCoun
     [e, (surjective_decode_iget (ι → ℕ)).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
     iUnion_univ_pi s, h2s, pi_univ]
 
+set_option trace.profiler true in
 /-- The product of generated σ-algebras is the one generated by boxes, if both generating sets
   are countably spanning. -/
 theorem generateFrom_pi_eq {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :
@@ -84,10 +85,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))

ℹ [847/847] Built Mathlib.MeasureTheory.MeasurableSpace.Pi (1.0s)
info: Mathlib/MeasureTheory/MeasurableSpace/Pi.lean:65:0: [Elab.async] [0.061781] elaborating proof of generateFrom_pi_eq
  [Elab.definition.value] [0.060351] generateFrom_pi_eq
    [Elab.step] [0.058500] classical
          cases nonempty_encodable ι
          apply le_antisymm
          · refine iSup_le ?_; intro i; rw [comap_generateFrom]
            apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
            choose t h1t h2t using hC
            simp_rw [eval_preimage, ← h2t]
            rw [← @iUnion_const _ ℕ _ s]
            have :
              Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
              by
              ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
              by_cases h : i' = i
              · subst h; simp
              · simp [h]
            rw [this, ← iUnion_univ_pi]
            apply MeasurableSet.iUnion
            intro n; apply measurableSet_generateFrom
            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))
            exact measurableSet_generateFrom (hs i (mem_univ i))
      [Elab.step] [0.058494] classical
            cases nonempty_encodable ι
            apply le_antisymm
            · refine iSup_le ?_; intro i; rw [comap_generateFrom]
              apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
              choose t h1t h2t using hC
              simp_rw [eval_preimage, ← h2t]
              rw [← @iUnion_const _ ℕ _ s]
              have :
                Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                  Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                by
                ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                by_cases h : i' = i
                · subst h; simp
                · simp [h]
              rw [this, ← iUnion_univ_pi]
              apply MeasurableSet.iUnion
              intro n; apply measurableSet_generateFrom
              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))
              exact measurableSet_generateFrom (hs i (mem_univ i))
        [Elab.step] [0.058486] classical
            cases nonempty_encodable ι
            apply le_antisymm
            · refine iSup_le ?_; intro i; rw [comap_generateFrom]
              apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
              choose t h1t h2t using hC
              simp_rw [eval_preimage, ← h2t]
              rw [← @iUnion_const _ ℕ _ s]
              have :
                Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                  Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                by
                ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                by_cases h : i' = i
                · subst h; simp
                · simp [h]
              rw [this, ← iUnion_univ_pi]
              apply MeasurableSet.iUnion
              intro n; apply measurableSet_generateFrom
              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))
              exact measurableSet_generateFrom (hs i (mem_univ i))
          [Elab.step] [0.058353] 
                cases nonempty_encodable ι
                apply le_antisymm
                · refine iSup_le ?_; intro i; rw [comap_generateFrom]
                  apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
                  choose t h1t h2t using hC
                  simp_rw [eval_preimage, ← h2t]
                  rw [← @iUnion_const _ ℕ _ s]
                  have :
                    Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                      Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                    by
                    ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                    by_cases h : i' = i
                    · subst h; simp
                    · simp [h]
                  rw [this, ← iUnion_univ_pi]
                  apply MeasurableSet.iUnion
                  intro n; apply measurableSet_generateFrom
                  apply mem_image_of_mem
                  grind
                · apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
[… 77 lines omitted …]
                          by_cases h : i' = i
                          · subst h; simp
                          · simp [h]
                        rw [this, ← iUnion_univ_pi]
                        apply MeasurableSet.iUnion
                        intro n; apply measurableSet_generateFrom
                        apply mem_image_of_mem
                        grind
                    [Elab.step] [0.013029] simp_rw [eval_preimage, ← h2t]
                    [Elab.step] [0.017060] have :
                          Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                            Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                          by
                          ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                          by_cases h : i' = i
                          · subst h; simp
                          · simp [h]
                      [Elab.step] [0.017044] focus
                            refine
                              no_implicit_lambda%
                                (have :
                                  Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                                    Set.pi univ fun k =>
                                      ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                                  ?body✝;
                                ?_)
                            case body✝ =>
                              with_annotate_state"by"
                                ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                  by_cases h : i' = i
                                  · subst h; simp
                                  · simp [h])
                        [Elab.step] [0.017040] 
                              refine
                                no_implicit_lambda%
                                  (have :
                                    Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                                      Set.pi univ fun k =>
                                        ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                                    ?body✝;
                                  ?_)
                              case body✝ =>
                                with_annotate_state"by"
                                  ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                    by_cases h : i' = i
                                    · subst h; simp
                                    · simp [h])
                          [Elab.step] [0.017038] 
                                refine
                                  no_implicit_lambda%
                                    (have :
                                      Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
                                        Set.pi univ fun k =>
                                          ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
                                      ?body✝;
                                    ?_)
                                case body✝ =>
                                  with_annotate_state"by"
                                    ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                      by_cases h : i' = i
                                      · subst h; simp
                                      · simp [h])
                            [Elab.step] [0.014312] case body✝ =>
                                  with_annotate_state"by"
                                    ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                      by_cases h : i' = i
                                      · subst h; simp
                                      · simp [h])
                              [Elab.step] [0.014280] with_annotate_state"by"
                                      ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                        by_cases h : i' = i
                                        · subst h; simp
                                        · simp [h])
                                [Elab.step] [0.014277] with_annotate_state"by"
                                        ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                          by_cases h : i' = i
                                          · subst h; simp
                                          · simp [h])
                                  [Elab.step] [0.014275] with_annotate_state"by"
                                        ( ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                          by_cases h : i' = i
                                          · subst h; simp
                                          · simp [h])
                                    [Elab.step] [0.014273] (
                                          ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                          by_cases h : i' = i
                                          · subst h; simp
                                          · simp [h])
                                      [Elab.step] [0.014270] 
                                            ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                            by_cases h : i' = i
                                            · subst h; simp
                                            · simp [h]
                                        [Elab.step] [0.014264] 
                                              ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
                                              by_cases h : i' = i
                                              · subst h; simp
                                              · simp [h]
                    [Elab.step] [0.011757] grind
Build completed successfully (847 jobs).

---

[github-actions]

PR summary 09610fd365

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jcommelin]

Thanks 🎉

bors merge