Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -11,7 +11,6 @@ import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.Lecture4
 import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM
-import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Copy
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.PlainCombi.KatonaCircle

LeanCamCombi/ExtrProbCombi/BinomialRandomGraph.lean

@@ -69,12 +69,14 @@ protected nonrec lemma meas [IsProbabilityMeasure μ] [Fintype α] [DecidableEq
     [DecidableRel H.Adj] :
     μ {ω | G ω = H} =
       p ^ #H.edgeFinset * (1 - p) ^ (Fintype.card {e : Sym2 α // ¬ e.IsDiag} - #H.edgeFinset) := by
-  have := hG.meas
-    (H.edgeFinset.attach.map <| ⟨Set.inclusion fun e he ↦
-      not_isDiag_of_mem_edgeSet _ <| mem_edgeFinset.1 he, Set.inclusion_injective _⟩)
-  simp at this
-  rw [Finset.card_attach, ← Fintype.card_subtype_compl] at this
-  convert this
-  sorry
+  have hHaux : H.edgeFinset = ({e | e ∈ H.edgeSet} : Finset _) := by ext; simp
+  have hGHaux ω : G ω = H ↔ {e : {e : Sym2 α // ¬ e.IsDiag} | e.1 ∈ (G ω).edgeSet} =
+    Set.range fun a : H.edgeFinset ↦
+      Set.inclusion (fun e he ↦ not_isDiag_of_mem_edgeSet H (mem_edgeFinset.mp he)) a := by
+    simp only [Set.ext_iff, ← edgeSet_inj]
+    simpa [Sym2.forall] using forall₂_congr fun u v ↦ by simp +contextual [or_iff_not_imp_left]
+  simpa [hGHaux, hHaux, ← Fintype.card_subtype_compl] using
+    hG.meas <| H.edgeFinset.attach.map <| ⟨Set.inclusion fun e he ↦
+      not_isDiag_of_mem_edgeSet _ <| mem_edgeFinset.1 he, Set.inclusion_injective _⟩
 
 end IsBinomialRandomGraph

LeanCamCombi/ExtrProbCombi/BollobasContainment.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
+import Mathlib.Combinatorics.SimpleGraph.Copy
 import Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.ExtrProbCombi.BinomialRandomGraph
-import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Copy
 
 /-!
 # Bollobás' graph containment lemma

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d22bd4f990c36ec29867ef381dc67f43c3d40520",
+   "rev": "6d323eaab8473e64720e30cd8e879e31d3817932",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ba020ed434b9c5877eb62ff072a28f5ec56eb871",
+   "rev": "8d29bc2c3ebe1f863c2f02df816b4f3dd1b65226",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "471ff276892c3451a1d693477107e9c3a0c8ab85",
+   "rev": "ecaaeb0b44a8d5784f17bd417e83f44c906804ab",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71c64425f2f76c4ffcf4a2f12b17c083976caaa0",
+   "rev": "7ad3747bf6cb10bfe96a40186ca8970ee851eb3b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",