Skip to content

Commit

Permalink
Bump mathlib
Browse files Browse the repository at this point in the history
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
zeramorphic committed Jan 8, 2025
1 parent d317c6b commit 51c38ad
Show file tree
Hide file tree
Showing 5 changed files with 80 additions and 79 deletions.
13 changes: 7 additions & 6 deletions ConNF/Background/Ordinal.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 α :=
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Background/Transfer.lean
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import Mathlib.Logic.Equiv.TransferInstance
import Mathlib.Algebra.Equiv.TransferInstance
import ConNF.Background.Ordinal

universe u v
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Base/Params.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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?
Expand Down
140 changes: 70 additions & 70 deletions lake-manifest.json
Original file line number Diff line number Diff line change
@@ -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"}
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.15.0-rc1
leanprover/lean4:v4.16.0-rc1

0 comments on commit 51c38ad

Please sign in to comment.