From 4b1c1deea42a0480e4cd3c1cb61d21a8c38a8e58 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Tue, 19 Nov 2024 21:59:18 +0000 Subject: [PATCH] Bump mathlib Signed-off-by: zeramorphic --- ConNF/Basic/InductiveConstruction.lean | 7 ++-- ConNF/Basic/Ordinal.lean | 34 ++++---------------- ConNF/Basic/Transfer.lean | 44 ++++++++------------------ ConNF/Counting/Conclusions.lean | 2 +- ConNF/Counting/SMulSpec.lean | 7 ++-- ConNF/FOA/BaseApprox.lean | 4 +-- ConNF/FOA/StrApprox.lean | 2 +- ConNF/FOA/StrApproxFOA.lean | 4 +-- ConNF/Setup/Deny.lean | 2 +- ConNF/Setup/Params.lean | 21 ++++++------ ConNF/Setup/Small.lean | 2 +- ConNF/Setup/StrSet.lean | 4 +-- ConNF/Setup/TypeIndex.lean | 2 +- lake-manifest.json | 38 ++++++++++++++-------- lean-toolchain | 2 +- 15 files changed, 76 insertions(+), 99 deletions(-) diff --git a/ConNF/Basic/InductiveConstruction.lean b/ConNF/Basic/InductiveConstruction.lean index 65a2bb0ab0..4c71e7c8f5 100644 --- a/ConNF/Basic/InductiveConstruction.lean +++ b/ConNF/Basic/InductiveConstruction.lean @@ -22,7 +22,10 @@ structure IndHyp (i : I) (t : ∀ j, r j i → Part (α j)) : Prop where (λ k h' ↦ (t k (Trans.trans h' h)).get (dom k _)) def core : ∀ i, Part (α i) := - inst.fix λ i t ↦ ⟨IndHyp i t, λ h ↦ f i (λ j h' ↦ (t j h').get (h.dom j h')) h.prop⟩ + inst.fix _ λ i t ↦ { + Dom := IndHyp i t + get := λ h ↦ f i (λ j h' ↦ (t j h').get (h.dom j h')) h.prop + } theorem core_eq (i : I) : core f i = ⟨IndHyp i (λ j _ ↦ core f j), @@ -38,7 +41,7 @@ theorem core_get_eq (i : I) (h : (core f i).Dom) : exact h.symm theorem core_dom (hp : ∀ i d h, p i (f i d h) d) : ∀ i, (core f i).Dom := by - refine inst.fix ?_ + refine inst.fix _ ?_ intro i ih rw [core_eq] refine ⟨ih, ?_⟩ diff --git a/ConNF/Basic/Ordinal.lean b/ConNF/Basic/Ordinal.lean index e4f90cec00..5c62ee862a 100644 --- a/ConNF/Basic/Ordinal.lean +++ b/ConNF/Basic/Ordinal.lean @@ -1,5 +1,6 @@ import ConNF.Basic.WellOrder -import Mathlib.SetTheory.Cardinal.Ordinal +import Mathlib.SetTheory.Cardinal.Aleph +import Mathlib.SetTheory.Cardinal.Arithmetic noncomputable section universe u v @@ -54,7 +55,7 @@ theorem isLimit_iff_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWell theorem type_Iio_lt {α : Type u} [LtWellOrder α] (x : α) : type (Subrel ((· < ·) : α → α → Prop) (Set.Iio x)) < type ((· < ·) : α → α → Prop) := - typein_lt_type _ x + @typein_lt_type _ _ (inferInstanceAs (IsWellOrder α (· < ·))) x def iicOrderIso {α : Type u} [LtWellOrder α] (x : α) : (Subrel ((· < ·) : α → α → Prop) (Set.Iic x)) ≃r @@ -93,29 +94,6 @@ theorem type_Iic_lt {α : Type u} [LtWellOrder α] [NoMaxOrder α] (x : α) : ## Lifting ordinals -/ -@[simp] -theorem typein_ordinal (o : Ordinal.{u}) : - -- TODO: Why can't Lean find this instance? - letI := inferInstanceAs (IsWellOrder Ordinal (· < ·)) - typein (· < ·) o = lift.{u + 1} o := by - letI := inferInstanceAs (IsWellOrder Ordinal (· < ·)) - induction o using Ordinal.induction with - | h o ih => - apply le_antisymm - · by_contra! h - have := ih (enum ((· < ·) : Ordinal → Ordinal → Prop) - ⟨lift.{u + 1} o, h.trans (typein_lt_type _ o)⟩) ?_ - · simp only [typein_enum, lift_inj] at this - conv_rhs at h => rw [this] - simp only [typein_enum, lt_self_iff_false] at h - · conv_rhs => rw [← enum_typein (· < ·) o] - exact enum_lt_enum.mpr h - · by_contra! h - rw [Ordinal.lt_lift_iff] at h - obtain ⟨o', ho'₁, ho'₂⟩ := h - rw [← ih o' ho'₂, typein_inj] at ho'₁ - exact ho'₂.ne ho'₁ - instance ULift.isTrichotomous {α : Type u} {r : α → α → Prop} [IsTrichotomous α r] : IsTrichotomous (ULift.{v} α) (InvImage r ULift.down) := by constructor @@ -158,7 +136,7 @@ theorem lift_typein_apply {α : Type u} {β : Type v} {r : α → α → Prop} { obtain ⟨y, hy⟩ := f.mem_range_of_rel x.down.prop refine ⟨ULift.up ⟨y, ?_⟩, ?_⟩ · have := x.down.prop - rwa [Set.mem_setOf_eq, ← hy, f.map_rel_iff] at this + rwa [← hy, f.map_rel_iff] at this · apply ULift.down_injective apply Subtype.coe_injective simp only [Set.mem_setOf_eq, Set.coe_setOf, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] @@ -179,7 +157,7 @@ theorem type_Iio (o : Ordinal.{u}) : have := Ordinal.lift_type_eq.{u + 1, u, u + 1} (r := ((· < ·) : Set.Iio o → Set.Iio o → Prop)) (s := ((· < ·) : o.toType → o.toType → Prop)) - rw [lift_id, type_lt] at this + rw [lift_id, type_toType] at this rw [this] exact ⟨o.enumIsoToType.toRelIsoLT⟩ @@ -243,7 +221,7 @@ def iioAddMonoid : AddMonoid (Set.Iio c.ord) where __ := iioZero h theorem nat_lt_ord (h : ℵ₀ ≤ c) (n : ℕ) : n < c.ord := by - apply (nat_lt_omega n).trans_le + apply (nat_lt_omega0 n).trans_le apply ord_mono at h rwa [ord_aleph0] at h diff --git a/ConNF/Basic/Transfer.lean b/ConNF/Basic/Transfer.lean index 1594039651..ea2fa06bc9 100644 --- a/ConNF/Basic/Transfer.lean +++ b/ConNF/Basic/Transfer.lean @@ -24,46 +24,30 @@ theorem lt_def [LT β] (x y : α) : Iff.rfl protected def min [Min β] : Min α where - min x y := e.symm (min (e x) (e y)) + min x y := e.symm (e x ⊓ e y) theorem min_def [Min β] (x y : α) : letI := e.min - min x y = e.symm (min (e x) (e y)) := - rfl - -protected def max [Max β] : Max α where - max x y := e.symm (max (e x) (e y)) - -theorem max_def [Max β] (x y : α) : - letI := e.max - max x y = e.symm (max (e x) (e y)) := - rfl - -protected def inf [Inf β] : Inf α where - inf x y := e.symm (e x ⊓ e y) - -theorem inf_def [Inf β] (x y : α) : - letI := e.inf x ⊓ y = e.symm (e x ⊓ e y) := rfl -theorem apply_inf [Inf β] (x y : α) : - letI := e.inf +theorem apply_min [Min β] (x y : α) : + letI := e.min e (x ⊓ y) = e x ⊓ e y := by - rw [inf_def, apply_symm_apply] + rw [min_def, apply_symm_apply] -protected def sup [Sup β] : Sup α where - sup x y := e.symm (e x ⊔ e y) +protected def max [Max β] : Max α where + max x y := e.symm (e x ⊔ e y) -theorem sup_def [Sup β] (x y : α) : - letI := e.sup +theorem max_def [Max β] (x y : α) : + letI := e.max x ⊔ y = e.symm (e x ⊔ e y) := rfl -theorem apply_sup [Sup β] (x y : α) : - letI := e.sup +theorem apply_max [Max β] (x y : α) : + letI := e.max e (x ⊔ y) = e x ⊔ e y := by - rw [sup_def, apply_symm_apply] + rw [max_def, apply_symm_apply] protected def compare [Ord β] : Ord α where compare x y := compare (e x) (e y) @@ -107,10 +91,10 @@ protected def partialOrder [PartialOrder β] : PartialOrder α := PartialOrder.lift e e.injective protected def linearOrder [LinearOrder β] : LinearOrder α := - letI := e.sup - letI := e.inf + letI := e.max + letI := e.min letI := e.compare - LinearOrder.liftWithOrd e e.injective e.apply_sup e.apply_inf e.compare_def + LinearOrder.liftWithOrd e e.injective e.apply_max e.apply_min e.compare_def protected def ltWellOrder [LtWellOrder β] : LtWellOrder α where wf := InvImage.wf e (inferInstanceAs <| IsWellFounded β (· < ·)).wf diff --git a/ConNF/Counting/Conclusions.lean b/ConNF/Counting/Conclusions.lean index f271727ac9..00a873babf 100644 --- a/ConNF/Counting/Conclusions.lean +++ b/ConNF/Counting/Conclusions.lean @@ -26,7 +26,7 @@ theorem card_codingFunction (β : TypeIndex) [LeLevel β] : revert β intro β induction β using WellFoundedLT.induction - case a β ih => + case ind β ih => intro cases β using WithBot.recBotCoe case bot => exact card_bot_codingFunction_lt diff --git a/ConNF/Counting/SMulSpec.lean b/ConNF/Counting/SMulSpec.lean index a8b6d164cf..55a4c76967 100644 --- a/ConNF/Counting/SMulSpec.lean +++ b/ConNF/Counting/SMulSpec.lean @@ -75,8 +75,7 @@ theorem inflexible_of_inflexible_smul {A : β ↝ ⊥} {N₁ N₂ : NearLitter} theorem litter_eq_of_flexible_smul {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : NearLitter} (h₁₂ : convNearLitters S (ρᵁ • S) A N₁ N₂) (h₃₄ : convNearLitters S (ρᵁ • S) A N₃ N₄) - (h₁ : ¬Inflexible A N₁ᴸ) (h₂ : ¬Inflexible A N₂ᴸ) - (h₃ : ¬Inflexible A N₃ᴸ) (h₄ : ¬Inflexible A N₄ᴸ) (h₁₃ : N₁ᴸ = N₃ᴸ) : + (h₁₃ : N₁ᴸ = N₃ᴸ) : N₂ᴸ = N₄ᴸ := by rw [convNearLitters_smul_iff_left] at h₁₂ h₃₄ rw [h₁₂.2, h₃₄.2, BasePerm.smul_nearLitter_litter, BasePerm.smul_nearLitter_litter, h₁₃] @@ -131,7 +130,9 @@ theorem sameSpecLe_smul : case convAtoms_injective => exact S.smul_convAtoms_injective ρ case atomMemRel_le => exact S.atomMemRel_smul_le ρ case inflexible_of_inflexible => exact S.inflexible_of_inflexible_smul ρ - case litter_eq_of_flexible => exact S.litter_eq_of_flexible_smul ρ + case litter_eq_of_flexible => + intros + apply S.litter_eq_of_flexible_smul ρ <;> assumption case atoms_of_inflexible => exact S.atoms_of_inflexible_smul ρ case nearLitters_of_inflexible => exact S.nearLitters_of_inflexible_smul ρ diff --git a/ConNF/FOA/BaseApprox.lean b/ConNF/FOA/BaseApprox.lean index cca2e6a4ec..b4ada47eb1 100644 --- a/ConNF/FOA/BaseApprox.lean +++ b/ConNF/FOA/BaseApprox.lean @@ -510,9 +510,9 @@ def upperBound (c : Set BaseApprox) (hc : IsChain (· ≤ ·) c) : BaseApprox wh exceptions := ⨆ ψ ∈ c, ψ.exceptions litters := ⨆ ψ ∈ c, ψᴸ exceptions_permutative := biSup_permutative_of_isChain - (λ ψ _ ↦ ψ.exceptions_permutative) (hc.image _ _ (λ _ _ h ↦ h.1.le)) + (λ ψ _ ↦ ψ.exceptions_permutative) (hc.image _ _ _ (λ _ _ h ↦ h.1.le)) litters_permutative' := biSup_permutative_of_isChain - (λ ψ _ ↦ ψ.litters_permutative) (hc.image _ _ (λ _ _ h ↦ h.2)) + (λ ψ _ ↦ ψ.litters_permutative) (hc.image _ _ _ (λ _ _ h ↦ h.2)) exceptions_small := upperBound_exceptions_small c hc theorem le_upperBound (c : Set BaseApprox) (hc : IsChain (· ≤ ·) c) : diff --git a/ConNF/FOA/StrApprox.lean b/ConNF/FOA/StrApprox.lean index f6a4066fcc..b1c3a085a1 100644 --- a/ConNF/FOA/StrApprox.lean +++ b/ConNF/FOA/StrApprox.lean @@ -61,7 +61,7 @@ end addOrbit /-- An upper bound for a chain of approximations. -/ def upperBound (c : Set (StrApprox β)) (hc : IsChain (· ≤ ·) c) : StrApprox β := - λ A ↦ BaseApprox.upperBound ((· A) '' c) (hc.image _ _ (λ _ _ h ↦ h A)) + λ A ↦ BaseApprox.upperBound ((· A) '' c) (hc.image _ _ _ (λ _ _ h ↦ h A)) theorem le_upperBound (c : Set (StrApprox β)) (hc : IsChain (· ≤ ·) c) : ∀ ψ ∈ c, ψ ≤ upperBound c hc := diff --git a/ConNF/FOA/StrApproxFOA.lean b/ConNF/FOA/StrApproxFOA.lean index 4fc8abda13..46c2406bf3 100644 --- a/ConNF/FOA/StrApproxFOA.lean +++ b/ConNF/FOA/StrApproxFOA.lean @@ -364,7 +364,7 @@ theorem exists_exactlyApproximates_of_total (ψ : StrApprox β) (hψ₁ : ψ.Coh revert β intro β induction β using (inferInstanceAs <| IsWellFounded TypeIndex (· < ·)).induction - case a _ _ β ih => + case ind _ _ β ih => induction β using WithBot.recBotCoe with | bot => intro _ ψ _ hψ₂ @@ -420,7 +420,7 @@ theorem freedomOfAction : FreedomOfAction β := by revert β intro β induction β using (inferInstanceAs <| IsWellFounded TypeIndex (· < ·)).induction - case a _ _ β ih => + case ind _ _ β ih => intro _ ψ hψ obtain ⟨χ, hχ₁, hχ₂, hχ₃⟩ := exists_total ψ hψ ih obtain ⟨ρ, hρ⟩ := exists_exactlyApproximates_of_total χ hχ₂ hχ₃ diff --git a/ConNF/Setup/Deny.lean b/ConNF/Setup/Deny.lean index 102cfad4c2..93ec5ba91c 100644 --- a/ConNF/Setup/Deny.lean +++ b/ConNF/Setup/Deny.lean @@ -31,7 +31,7 @@ theorem initialWellOrder_type {X : Type _} : letI := initialWellOrder X type ((· < ·) : X → X → Prop) = (#X).ord := by have := Equiv.ltWellOrder_type (initialEquiv (X := X)) - rwa [Ordinal.lift_id, Ordinal.lift_id, type_lt] at this + rwa [Ordinal.lift_id, Ordinal.lift_id, type_toType] at this theorem initialWellOrder_card_Iio {X : Type _} : letI := initialWellOrder X diff --git a/ConNF/Setup/Params.lean b/ConNF/Setup/Params.lean index 7ba901f93b..35c6f24b34 100644 --- a/ConNF/Setup/Params.lean +++ b/ConNF/Setup/Params.lean @@ -46,22 +46,23 @@ def Params.minimal : Params where rw [mk_out] exact isRegular_aleph_one μ_isStrongLimit := by - rw [mk_out] - exact isStrongLimit_beth <| IsLimit.isSuccPrelimit <| ord_aleph_isLimit 1 + rw [mk_out, ord_aleph] + exact isStrongLimit_beth <| IsLimit.isSuccPrelimit <| isLimit_omega 1 κ_lt_μ := by - rw [mk_out, mk_out] + rw [mk_out, mk_out, ord_aleph] apply (aleph_le_beth 1).trans_lt rw [beth_strictMono.lt_iff_lt] - exact (ord_aleph_isLimit 1).one_lt + exact (isLimit_omega 1).one_lt κ_le_μ_ord_cof := by rw [mk_out, mk_out] - have := beth_normal.cof_le (aleph 1).ord + have := isNormal_beth.cof_le (aleph 1).ord rwa [isRegular_aleph_one.cof_eq] at this Λ_type_le_μ_ord_cof := by rw [type_nat_lt, mk_out] - have := beth_normal.cof_le (aleph 1).ord + apply (omega0_le_of_isLimit (isLimit_omega 1)).trans + have := isNormal_beth.cof_le (aleph 1).ord rw [isRegular_aleph_one.cof_eq, ← ord_le_ord] at this - exact (omega_le_of_isLimit (ord_aleph_isLimit 1)).trans this + rwa [ord_aleph] at this ⊢ def Params.inaccessible.{v} : Params where Λ := (Cardinal.univ.{v, v + 1}).ord.toType @@ -73,8 +74,8 @@ def Params.inaccessible.{v} : Params where Λ_noMaxOrder := by apply noMaxOrder_of_isLimit change (type ((· < ·) : (Cardinal.univ.{v, v + 1}).ord.toType → _ → Prop)).IsLimit - rw [type_lt] - apply ord_isLimit + rw [type_toType] + apply isLimit_ord exact univ_inaccessible.1.le aleph0_lt_κ := by rw [mk_uLift, mk_out, ← lift_aleph0.{v + 1, v}, lift_strictMono.lt_iff_lt] @@ -94,7 +95,7 @@ def Params.inaccessible.{v} : Params where exact (lift_lt_univ _).le Λ_type_le_μ_ord_cof := by change type ((· < ·) : (Cardinal.univ.{v, v + 1}).ord.toType → _ → Prop) ≤ _ - rw [type_lt, mk_out, univ_inaccessible.2.1.cof_eq] + rw [type_toType, mk_out, univ_inaccessible.2.1.cof_eq] export Params (Λ κ μ aleph0_lt_κ κ_isRegular μ_isStrongLimit κ_lt_μ κ_le_μ_ord_cof Λ_type_le_μ_ord_cof) diff --git a/ConNF/Setup/Small.lean b/ConNF/Setup/Small.lean index 9df512253d..7e586b202b 100644 --- a/ConNF/Setup/Small.lean +++ b/ConNF/Setup/Small.lean @@ -35,7 +35,7 @@ theorem Small.lt : Small s → #s < #κ := -/ theorem small_of_subsingleton (h : s.Subsingleton) : Small s := - h.cardinal_mk_le_one.trans_lt <| one_lt_aleph0.trans_le aleph0_lt_κ.le + h.cardinalMk_le_one.trans_lt <| one_lt_aleph0.trans_le aleph0_lt_κ.le @[simp] theorem small_empty : Small (∅ : Set α) := diff --git a/ConNF/Setup/StrSet.lean b/ConNF/Setup/StrSet.lean index e0723e1269..f36335cc2e 100644 --- a/ConNF/Setup/StrSet.lean +++ b/ConNF/Setup/StrSet.lean @@ -94,7 +94,7 @@ theorem strPerm_smul_coe {α : Λ} (π : StrPerm α) (x : StrSet α) : theorem one_strPerm_smul {α : TypeIndex} (x : StrSet α) : strPerm_smul 1 x = x := by induction α using WellFoundedLT.induction - case a α ih => + case ind α ih => cases α using WithBot.recBotCoe case bot => rw [strPerm_smul_bot_def, Tree.one_apply, one_smul, Equiv.symm_apply_apply] case coe α => @@ -105,7 +105,7 @@ theorem one_strPerm_smul {α : TypeIndex} (x : StrSet α) : strPerm_smul 1 x = x theorem mul_strPerm_smul {α : TypeIndex} (π₁ π₂ : StrPerm α) (x : StrSet α) : strPerm_smul (π₁ * π₂) x = strPerm_smul π₁ (strPerm_smul π₂ x) := by induction α using WellFoundedLT.induction - case a α ih => + case ind α ih => cases α using WithBot.recBotCoe case bot => simp only [strPerm_smul_bot_def, Tree.mul_apply, mul_smul, Equiv.apply_symm_apply] diff --git a/ConNF/Setup/TypeIndex.lean b/ConNF/Setup/TypeIndex.lean index ff161ef3f0..e6750058e6 100644 --- a/ConNF/Setup/TypeIndex.lean +++ b/ConNF/Setup/TypeIndex.lean @@ -34,7 +34,7 @@ instance : WellFoundedRelation TypeIndex where protected theorem TypeIndex.type : type ((· < ·) : TypeIndex → TypeIndex → Prop) = type ((· < ·) : Λ → Λ → Prop) := by rw [type_withBot] - exact one_add_of_omega_le <| omega_le_of_isLimit Λ_type_isLimit + exact one_add_of_omega0_le <| omega0_le_of_isLimit Λ_type_isLimit @[simp] protected theorem TypeIndex.card : diff --git a/lake-manifest.json b/lake-manifest.json index 370760cb88..02212afa06 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4756e0fc48acce0cc808df0ad149de5973240df6", + "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad", + "rev": "de91b59101763419997026c35a41432ac8691f15", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,17 +35,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", + "rev": "1383e72b40dd62a566896a6e348ffe868801b172", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.42", + "inputRev": "v0.0.46", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "", - "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", + "scope": "leanprover", + "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1", + "rev": "119b022b3ea88ec810a677888528e50f8144a26e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,17 +65,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "781beceb959c68b36d3d96205b3531e341879d2c", + "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "bb7a404341c1b8f113a011a0a60b367b7d2649ff", + "rev": "29f545b8110e796db8de688fa9e3950ce95cf678", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -95,7 +105,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0", + "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,7 +115,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8", + "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -115,7 +125,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5119580cd7510a440d54f67834c9024cc03a3e32", + "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 89985206ac..57a4710c03 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0 +leanprover/lean4:v4.14.0-rc2