From 51c38ad244870b8b1f40b8272b281678397dfa4f Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 8 Jan 2025 14:22:48 +0000 Subject: [PATCH] Bump mathlib Signed-off-by: zeramorphic --- ConNF/Background/Ordinal.lean | 13 +-- ConNF/Background/Transfer.lean | 2 +- ConNF/Base/Params.lean | 2 +- lake-manifest.json | 140 ++++++++++++++++----------------- lean-toolchain | 2 +- 5 files changed, 80 insertions(+), 79 deletions(-) diff --git a/ConNF/Background/Ordinal.lean b/ConNF/Background/Ordinal.lean index a8980c2b68..d3d774e16b 100644 --- a/ConNF/Background/Ordinal.lean +++ b/ConNF/Background/Ordinal.lean @@ -42,12 +42,13 @@ theorem noMaxOrder_of_isLimit {α : Type u} [Preorder α] [IsWellOrder α (· < theorem isLimit_of_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWellOrder α (· < ·)] (h : NoMaxOrder α) : (type ((· < ·) : α → α → Prop)).IsLimit := by constructor - · simp only [ne_eq, type_eq_zero_iff_isEmpty, not_isEmpty_of_nonempty, not_false_eq_true] + · simp only [isMin_iff_eq_bot, bot_eq_zero, type_eq_zero_iff_isEmpty, not_isEmpty_of_nonempty, + not_false_eq_true] · intro o ho - obtain ⟨x, hx⟩ := h.exists_gt (enum ((· < ·) : α → α → Prop) ⟨o, ho⟩) - refine lt_of_le_of_lt ?_ (typein_lt_type ((· < ·) : α → α → Prop) x) - rw [← typein_lt_typein ((· < ·) : α → α → Prop), typein_enum] at hx - rwa [Order.succ_le_iff] + obtain ⟨x, hx⟩ := h.exists_gt (enum ((· < ·) : α → α → Prop) ⟨o, ho.1⟩) + have := ho.2 + refine this ?_ (typein_lt_type ((· < ·) : α → α → Prop) x) + rwa [← typein_lt_typein ((· < ·) : α → α → Prop), typein_enum] at hx theorem isLimit_iff_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWellOrder α (· < ·)] : (type ((· < ·) : α → α → Prop)).IsLimit ↔ NoMaxOrder α := @@ -88,7 +89,7 @@ theorem type_Iic_lt {α : Type u} [LtWellOrder α] [NoMaxOrder α] (x : α) : rw [type_Iic_eq] haveI : Nonempty α := ⟨x⟩ have h := isLimit_of_noMaxOrder (inferInstanceAs (NoMaxOrder α)) - exact h.right _ (type_Iio_lt x) + exact h.2.succ_lt (type_Iio_lt x) /-! ## Lifting ordinals diff --git a/ConNF/Background/Transfer.lean b/ConNF/Background/Transfer.lean index b4665ae092..02da0c823c 100644 --- a/ConNF/Background/Transfer.lean +++ b/ConNF/Background/Transfer.lean @@ -1,4 +1,4 @@ -import Mathlib.Logic.Equiv.TransferInstance +import Mathlib.Algebra.Equiv.TransferInstance import ConNF.Background.Ordinal universe u v diff --git a/ConNF/Base/Params.lean b/ConNF/Base/Params.lean index e98bbdb807..8510dfef71 100644 --- a/ConNF/Base/Params.lean +++ b/ConNF/Base/Params.lean @@ -334,7 +334,7 @@ instance : IsLeftCancelAdd κ := by intro x y z h rw [← κEquiv.apply_eq_iff_eq, ← Subtype.coe_inj] at h ⊢ rw [κEquiv_add, κEquiv_add] at h - exact (Ordinal.add_left_cancel _).mp h + exact add_left_cancel_iff.mp h theorem κ_typein (x : κ) : -- TODO: Why can't Lean find this instance? diff --git a/lake-manifest.json b/lake-manifest.json index 73abcdf15b..232a81caa9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,135 +1,135 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83", - "name": "batteries", + "scope": "", + "rev": "27bf1dcda3cc28d908608e4b9c09daca3aaa50aa", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", - "name": "Qq", + "scope": "", + "rev": "0fe74732b679f28f3cf40e9886154358182c25b9", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", - "inherited": true, + "inputRev": null, + "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "8b6048aa0a4a4b6bcf83597802d8dee734e64b7e", - "name": "aesop", + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "2b000e02d50394af68cfb4770a291113d94801b5", - "name": "proofwidgets", + "scope": "", + "rev": "b64b8eab8cfcf24c398e84b11c77b6555b61095a", + "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.48", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", + "scope": "", + "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", - "name": "importGraph", + "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155", + "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", - "name": "plausible", + "rev": "9cb79405471ae931ac718231d6299bfaffef9087", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "de7196a7d290d6269d4d5f1130a3d0a8c29414ce", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", - "name": "MD4Lean", + "scope": "leanprover-community", + "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.50", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", - "name": "UnicodeBasic", + "scope": "leanprover-community", + "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.16.0-rc1", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "scope": "", - "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", - "name": "BibtexQuery", + "scope": "leanprover-community", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", + "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.15.0", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "099b90e374ba73983c3fda87595be625f1931669", - "name": "«doc-gen4»", + "scope": "leanprover-community", + "rev": "b2e8b6868397fcd93c00aca7278b933c16c0ffb3", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], + "inputRev": "v4.16.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "ConNF", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index cf25a9816f..62ccd7170e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 +leanprover/lean4:v4.16.0-rc1