Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -15,8 +15,6 @@ import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
-import LeanCamCombi.Mathlib.Data.Fintype.Card
-import LeanCamCombi.Mathlib.Data.Nat.Choose.Cast
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.PlainCombi.KatonaCircle
 import LeanCamCombi.PlainCombi.LittlewoodOfford

LeanCamCombi/ExtrProbCombi/BernoulliSeq.lean

@@ -33,7 +33,7 @@ variable {α Ω : Type*} [MeasurableSpace Ω]
 structure IsBernoulliSeq (X : Ω → Set α) (p : outParam ℝ≥0) (μ : Measure Ω := by volume_tac) : Prop
     where
   protected le_one : p ≤ 1
-  protected iIndepFun : iIndepFun inferInstance (fun a ω ↦ a ∈ X ω) μ
+  protected iIndepFun : iIndepFun (fun a ω ↦ a ∈ X ω) μ
   protected map : ∀ a, Measure.map (fun ω ↦ a ∈ X ω) μ = (PMF.bernoulli' p le_one).toMeasure
 
 variable {X Y : Ω → Set α} {μ : Measure Ω} {p q : ℝ≥0} (hX : IsBernoulliSeq X p μ)

LeanCamCombi/ExtrProbCombi/BinomialRandomGraph.lean

@@ -41,11 +41,9 @@ include hG
 protected nonrec lemma le_one : p ≤ 1 := hG.le_one
 
 lemma iIndepFun_mem_edgeSet_not_isDiag :
-    iIndepFun inferInstance (fun (e : {e : Sym2 α // ¬ e.IsDiag}) ω ↦ ↑e ∈ (G ω).edgeSet) μ :=
-  hG.iIndepFun
+    iIndepFun (fun (e : {e : Sym2 α // ¬ e.IsDiag}) ω ↦ ↑e ∈ (G ω).edgeSet) μ := hG.iIndepFun
 
-lemma iIndepFun_mem_edgeSet : iIndepFun inferInstance (fun e ω ↦ e ∈ (G ω).edgeSet) μ :=
-  sorry
+lemma iIndepFun_mem_edgeSet : iIndepFun (fun e ω ↦ e ∈ (G ω).edgeSet) μ := sorry
 
 lemma map_mem_edgeSet (he : ¬ e.IsDiag) :
     Measure.map (fun ω ↦ e ∈ (G ω).edgeSet) μ = (PMF.bernoulli' p hG.le_one).toMeasure :=

LeanCamCombi/Mathlib/Data/Fintype/Card.lean

@@ -3,11 +3,10 @@ Copyright (c) 2024 Ching-Tsun Chou, Chris Wong. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou, Chris Wong
 -/
-import LeanCamCombi.Mathlib.Data.Fintype.Card
-import LeanCamCombi.Mathlib.Data.Nat.Choose.Cast
 import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Perm
+import Mathlib.Data.Nat.Choose.Cast
 
 /-!
 # The Katona circle method
@@ -71,7 +70,7 @@ def prefixedEquiv (s : Finset α) : prefixed s ≃ Numbering s × Numbering ↑(
   invFun := fun (g, g') ↦
     { val.toFun x :=
         if hx : x ∈ s then
-          g ⟨x, hx⟩ |>.castLE Fintype.card_subtype_le'
+          g ⟨x, hx⟩ |>.castLE (Fintype.card_subtype_le _)
         else
           g' ⟨x, by simpa⟩ |>.addNat #s |>.cast (by simp [card_le_univ])
       val.invFun n :=
@@ -88,7 +87,7 @@ def prefixedEquiv (s : Finset α) : prefixed s ≃ Numbering s × Numbering ↑(
         obtain hns | hsn := lt_or_le n.1 #s
         · simp [hns]
         · simp [hsn.not_lt, hsn, dif_neg (mem_compl.1 <| Subtype.prop _), Fin.ext_iff,
-            Fintype.card_subtype_le']
+            Fintype.card_subtype_le]
       property := mem_prefixed.2 fun x ↦ by
         constructor
         · intro hx
@@ -107,7 +106,7 @@ lemma card_prefixed (s : Finset α) : #(prefixed s) = (#s)! * (card α - #s)! :=
 
 @[simp]
 lemma dens_prefixed (s : Finset α) : (prefixed s).dens = ((card α).choose #s : ℚ≥0)⁻¹ := by
-  simp [dens, card_prefixed, Nat.cast_choose' _ s.card_le_univ]
+  simp [dens, card_prefixed, Nat.cast_choose _ s.card_le_univ]
 
 -- TODO: This can be strengthened to an iff
 lemma disjoint_prefixed_prefixed (hst : ¬ s ⊆ t) (hts : ¬ t ⊆ s) :

LeanCamCombi/Mathlib/Data/Nat/Choose/Cast.lean

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
+   "rev": "3800f46f4b3baed8f14b0cd3a90963c5a453667b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.17.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
+   "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
+   "rev": "08372f1ec11df288ff76621ead7b0b575cb29355",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
+   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.52",
+   "inputRev": "v0.0.53",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
+   "rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
+   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
+   "rev": "cce013731b5b355ff4528ac9717ae3e0cc5c4519",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca",
+   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

LeanCamCombi/PlainCombi/KatonaCircle.lean

@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0-rc1