Bump mathlib

YaelDillies · Dec 21, 2023 · 667401f · 667401f
1 parent 8e2f38a
commit 667401f
Show file tree

Hide file tree

Showing 8 changed files with 8 additions and 83 deletions.
diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
@@ -47,7 +47,6 @@ import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
 import LeanCamCombi.Mathlib.GroupTheory.Subgroup.Stabilizer
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanCamCombi.Mathlib.Order.Category.BoolAlg
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic

diff --git a/LeanCamCombi/BernoulliSeq.lean b/LeanCamCombi/BernoulliSeq.lean
@@ -82,8 +82,8 @@ protected lemma meas [Fintype α] (s : Finset α) :
     Finset.prod_eq_pow_card, Finset.card_compl]
   · rintro a hi
     rw [Finset.mem_compl] at hi
-    simp only [hi, ←compl_setOf, NullMeasurableSet.prob_compl_eq_one_sub, mem_setOf_eq,
-      Finset.mem_coe, iff_false_iff, hX.nullMeasurableSet, hX.meas_apply]
+    simp only [hi, ←compl_setOf, prob_compl_eq_one_sub₀, mem_setOf_eq, Finset.mem_coe,
+      iff_false_iff, hX.nullMeasurableSet, hX.meas_apply]
   · rintro a hi
     simp only [hi, mem_setOf_eq, Finset.mem_coe, iff_true_iff, hX.meas_apply]
   rintro a

diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean
@@ -184,8 +184,8 @@ noncomputable def copyCount (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
   haveI : IsEmpty (⊥ : H.Subgraph).verts := by simp
   refine' ⟨⟨⟨⟨isEmptyElim, isEmptyElim, isEmptyElim, isEmptyElim⟩, fun {a} ↦ isEmptyElim a⟩⟩,
     fun H' e ↦ Subgraph.ext _ _ _ $ funext₂ fun a b ↦ _⟩
-  · simpa [Set.eq_empty_iff_forall_not_mem, filter_eq_empty_iff] using
-      Fintype.card_congr e.toEquiv.symm
+  · simpa [Set.eq_empty_iff_forall_not_mem, filter_eq_empty_iff, ‹IsEmpty α›] using
+      e.toEquiv.symm.isEmpty_congr
   · simp only [Subgraph.not_bot_adj, eq_iff_iff, iff_false_iff]
     exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe
 

diff --git a/LeanCamCombi/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/LeanCamCombi/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
diff --git a/LeanCamCombi/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/LeanCamCombi/Mathlib/MeasureTheory/Measure/Typeclasses.lean
@@ -1,13 +1,11 @@
 import Mathlib.MeasureTheory.Measure.Typeclasses
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 
 variable {α β : Type*} [MeasurableSpace β] {f g : α → β} {s : Set β}
 
 namespace MeasureTheory
 variable [MeasurableSpace α] {μ : Measure α} {s : Set α}
 
-lemma NullMeasurableSet.prob_compl_eq_one_sub [IsProbabilityMeasure μ] {s : Set α}
-    (h : NullMeasurableSet s μ) : μ (sᶜ) = 1 - μ s := by
-  rw [h.measure_compl (measure_ne_top _ _), measure_univ]
+lemma prob_compl_eq_one_sub₀ [IsProbabilityMeasure μ] {s : Set α} (h : NullMeasurableSet s μ) :
+    μ sᶜ = 1 - μ s := by rw [measure_compl₀ h (measure_ne_top _ _), measure_univ]
 
 end MeasureTheory
diff --git a/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean b/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean
@@ -1,5 +1,4 @@
 import Mathlib.Probability.Independence.Basic
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 
 open MeasureTheory MeasurableSpace Set
 open scoped BigOperators

diff --git a/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean b/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
@@ -1,5 +1,4 @@
 import Mathlib.Probability.ProbabilityMassFunction.Constructions
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 
 -- TODO: On a countable space, define one-to-one correspondance between `PMF` and probability
 -- measures

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "6b4cf96c89e53cfcd73350bbcd90333a051ff4f0",
+   "rev": "5bf9172331fb4de21647a919c64d3569839b63c6",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "4160b2aa344c39b1238e7c5da7227f763ac72b58",
+   "rev": "da34c254e89b2cde09d066068c17cf30ebe603f8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,