From 14694e8022214b899f81c1a48f5c4165db3262e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 14 Jun 2024 18:36:40 +0000 Subject: [PATCH] Bump mathlib --- LeanCamCombi.lean | 4 -- LeanCamCombi/Mathlib/Data/Nat/Factors.lean | 1 - LeanCamCombi/Mathlib/Data/Set/Image.lean | 5 -- .../Mathlib/Order/Category/BoolAlg.lean | 12 ----- LeanCamCombi/Mathlib/Order/Hom/Set.lean | 10 ---- LeanCamCombi/Mathlib/Order/SupClosed.lean | 52 ------------------- lake-manifest.json | 14 ++--- lean-toolchain | 2 +- 8 files changed, 8 insertions(+), 92 deletions(-) delete mode 100644 LeanCamCombi/Mathlib/Data/Nat/Factors.lean delete mode 100644 LeanCamCombi/Mathlib/Data/Set/Image.lean delete mode 100644 LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean delete mode 100644 LeanCamCombi/Mathlib/Order/Hom/Set.lean delete mode 100644 LeanCamCombi/Mathlib/Order/SupClosed.lean diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 4bfac0d6d9..3c7bb30fad 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -44,16 +44,12 @@ import LeanCamCombi.Mathlib.Data.List.Basic import LeanCamCombi.Mathlib.Data.List.DropRight import LeanCamCombi.Mathlib.Data.Multiset.Basic import LeanCamCombi.Mathlib.Data.Nat.Defs -import LeanCamCombi.Mathlib.Data.Nat.Factors import LeanCamCombi.Mathlib.Data.Set.Finite -import LeanCamCombi.Mathlib.Data.Set.Image import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul import LeanCamCombi.Mathlib.FieldTheory.Finite.Basic import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup -import LeanCamCombi.Mathlib.Order.Category.BoolAlg import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic import LeanCamCombi.Mathlib.Order.Hom.Lattice -import LeanCamCombi.Mathlib.Order.Hom.Set import LeanCamCombi.Mathlib.Order.Interval.Finset.Basic import LeanCamCombi.Mathlib.Order.Partition.Finpartition import LeanCamCombi.Mathlib.Order.Sublattice diff --git a/LeanCamCombi/Mathlib/Data/Nat/Factors.lean b/LeanCamCombi/Mathlib/Data/Nat/Factors.lean deleted file mode 100644 index 1e17c4e2c9..0000000000 --- a/LeanCamCombi/Mathlib/Data/Nat/Factors.lean +++ /dev/null @@ -1 +0,0 @@ --- TODO: Rename `Nat.factors` to `Nat.primeFactorsList` diff --git a/LeanCamCombi/Mathlib/Data/Set/Image.lean b/LeanCamCombi/Mathlib/Data/Set/Image.lean deleted file mode 100644 index 1db4acff85..0000000000 --- a/LeanCamCombi/Mathlib/Data/Set/Image.lean +++ /dev/null @@ -1,5 +0,0 @@ -/-! -### TODO - -Extra explicit arguments to `Subtype.range_coe`/`Subtype.range_val`. --/ diff --git a/LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean b/LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean deleted file mode 100644 index 24a5508111..0000000000 --- a/LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Mathlib.Order.Category.BoolAlg -import Mathlib.Order.Hom.CompleteLattice - -open CategoryTheory OrderDual Opposite Set - -universe u - -/-- The powerset functor. `Set` as a contravariant functor. -/ -def typeToBoolAlgOp : Type u ⥤ BoolAlgᵒᵖ where - obj X := op $ BoolAlg.of (Set X) - map {X Y} f := Quiver.Hom.op - (CompleteLatticeHom.setPreimage f : BoundedLatticeHom (Set Y) (Set X)) diff --git a/LeanCamCombi/Mathlib/Order/Hom/Set.lean b/LeanCamCombi/Mathlib/Order/Hom/Set.lean deleted file mode 100644 index 085c621599..0000000000 --- a/LeanCamCombi/Mathlib/Order/Hom/Set.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Mathlib.Order.Hom.Set - -open OrderDual - -section BooleanAlgebra -variable {α : Type*} [BooleanAlgebra α] - -@[simp] lemma OrderIso.compl_symm_apply' (a : αᵒᵈ) : (OrderIso.compl α).symm a = ofDual aᶜ := rfl - -end BooleanAlgebra diff --git a/LeanCamCombi/Mathlib/Order/SupClosed.lean b/LeanCamCombi/Mathlib/Order/SupClosed.lean deleted file mode 100644 index c024d7f8fe..0000000000 --- a/LeanCamCombi/Mathlib/Order/SupClosed.lean +++ /dev/null @@ -1,52 +0,0 @@ -import Mathlib.Data.Set.Finite -import Mathlib.Order.Hom.Lattice -import Mathlib.Order.SupClosed - -open OrderDual - -variable {α β : Type*} - -/-! ### Closure -/ - -section SemilatticeSup -variable [SemilatticeSup α] [SemilatticeSup β] {s t : Set α} {a b : α} - -open Finset - -@[simp] lemma supClosure_prod (s : Set α) (t : Set β) : - supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t := - le_antisymm (supClosure_min (Set.prod_mono subset_supClosure subset_supClosure) $ - supClosed_supClosure.prod supClosed_supClosure) $ by - rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩ - refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩ - · simpa only [coe_product] using Set.prod_mono hus hvt - · simp [prodMk_sup'_sup'] - -end SemilatticeSup - -section SemilatticeInf -variable [SemilatticeInf α] [SemilatticeInf β] {s t : Set α} {a b : α} - -open Finset - -@[simp] lemma infClosure_prod (s : Set α) (t : Set β) : - infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t := - le_antisymm (infClosure_min (Set.prod_mono subset_infClosure subset_infClosure) $ - infClosed_infClosure.prod infClosed_infClosure) $ by - rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩ - refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩ - · simpa only [coe_product] using Set.prod_mono hus hvt - · simp [prodMk_inf'_inf'] - -end SemilatticeInf - -section DistribLattice -variable [DistribLattice α] [DistribLattice β] {s : Set α} - -open Finset - -@[simp] lemma latticeClosure_prod (s : Set α) (t : Set β) : - latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t := by - simp_rw [← supClosure_infClosure]; simp - -end DistribLattice diff --git a/lake-manifest.json b/lake-manifest.json index 5c1bf79b73..99e00ecb3c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "6a63eb6a326181df29d95a84ce1f16c1145e66d8", + "rev": "15d42e1a92a80d0db5ca1c12123866ba392b9d76", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05", + "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -58,17 +58,17 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "ed63385753ed24f23d780e567364a1e001f6ee91", + "rev": "dff3a0ef1acdb1f34dd05dbaa41e620d22c6a3cf", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/xubaiw/CMark.lean", + {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, - "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05", - "name": "CMark", + "rev": "d812b96744f9b60879cbfa9c436de2b95003db2a", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -94,7 +94,7 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "4e570fed8c4147bdafbd5eada08503ed307252e0", + "rev": "b61771aaa8f15bce5e3a38aebeb6dda487f4f29c", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 0ba3faf807..29c0cea43e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0-rc1 +leanprover/lean4:v4.9.0-rc2