Bump mathlib

YaelDillies · Dec 27, 2023 · 1041902 · 1041902
1 parent d798edd
commit 1041902
Show file tree

Hide file tree

Showing 7 changed files with 3 additions and 72 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -33,15 +33,13 @@ import LeanAPAP.Mathlib.Analysis.NormedSpace.Ray
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.Complex.Order
-import LeanAPAP.Mathlib.Data.Finset.Basic
 import LeanAPAP.Mathlib.Data.Finset.Card
 import LeanAPAP.Mathlib.Data.Finset.Image
 import LeanAPAP.Mathlib.Data.Finset.Pi
 import LeanAPAP.Mathlib.Data.Finset.Pointwise
 import LeanAPAP.Mathlib.Data.Finset.Powerset
 import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Fintype.BigOperators
-import LeanAPAP.Mathlib.Data.Fintype.Card
 import LeanAPAP.Mathlib.Data.Fintype.Lattice
 import LeanAPAP.Mathlib.Data.Fintype.Pi
 import LeanAPAP.Mathlib.Data.FunLike.Basic

diff --git a/LeanAPAP/Mathlib/Data/Finset/Basic.lean b/LeanAPAP/Mathlib/Data/Finset/Basic.lean
diff --git a/LeanAPAP/Mathlib/Data/Fintype/Basic.lean b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean
@@ -7,11 +7,6 @@ namespace Finset
 @[simp]
 lemma filter_mem_univ (s : Finset α) : univ.filter (· ∈ s) = s := by simp [filter_mem_eq_inter]
 
--- @[simp] --TODO: Unsimp `finset.univ_unique`
-lemma singleton_eq_univ [Subsingleton α] (a : α) : ({a} : Finset α) = univ := by
-  ext b; simp [Subsingleton.elim a b]
+-- TODO: Unsimp `Finset.univ_unique`
 
 end Finset
-
-instance {s : Set α} [DecidablePred (· ∈ s)] : Decidable s.Subsingleton :=
-  decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, a = b) Iff.rfl
diff --git a/LeanAPAP/Mathlib/Data/Fintype/Card.lean b/LeanAPAP/Mathlib/Data/Fintype/Card.lean
diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean
@@ -293,7 +293,7 @@ noncomputable instance instFintype [Finite G] : Fintype (AddChar G R) :=
 
 @[simp] lemma card_addChar_le [Fintype G] : card (AddChar G R) ≤ card G := by
   simpa only [FiniteDimensional.finrank_fintype_fun_eq_card] using
-    FiniteDimensional.fintype_card_le_finrank_of_linearIndependent (AddChar.linearIndependent G R)
+    (AddChar.linearIndependent G R).fintype_card_le_finrank
 
 end IsROrC
 

diff --git a/LeanAPAP/Prereqs/Dissociation.lean b/LeanAPAP/Prereqs/Dissociation.lean
@@ -5,7 +5,6 @@ import Mathlib.Data.Fintype.Pi
 import Mathlib.Data.Set.Pointwise.Basic
 import LeanAPAP.Mathlib.Algebra.BigOperators.Basic
 import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
-import LeanAPAP.Mathlib.Data.Finset.Basic
 import LeanAPAP.Mathlib.Data.Finset.Powerset
 import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Set.Function

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -49,47 +49,11 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "be0b59d276020004e21109a79cab71f259755349",
+   "rev": "7a302eb97c8a48fef146f33f55eb00fc7a5541e3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-   "name": "CMark",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "LeanAPAP",
  "lakeDir": ".lake"}