diff --git a/Mathlib/Algebra/Category/Ring/Epi.lean b/Mathlib/Algebra/Category/Ring/Epi.lean index eaf70a8f1b5dc..4cba68f80ce52 100644 --- a/Mathlib/Algebra/Category/Ring/Epi.lean +++ b/Mathlib/Algebra/Category/Ring/Epi.lean @@ -24,7 +24,7 @@ lemma CommRingCat.epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S] constructor · intro H have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom (R := R)) - (CommRingCat.ofHom <| Algebra.TensorProduct.includeRight.toRingHom) + (CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom) (by ext r; show algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r; simp only [Algebra.algebraMap_eq_smul_one, smul_tmul]) exact RingHom.congr_fun this diff --git a/Mathlib/Algebra/Lie/Semisimple/Basic.lean b/Mathlib/Algebra/Lie/Semisimple/Basic.lean index 12b30d31de1c2..4de125bf588e1 100644 --- a/Mathlib/Algebra/Lie/Semisimple/Basic.lean +++ b/Mathlib/Algebra/Lie/Semisimple/Basic.lean @@ -212,7 +212,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal set K := s'.sup id suffices I ≤ K by obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this - exact ⟨t, hts'.trans hs'.subset, htI⟩ + exact ⟨t, Finset.Subset.trans hts' hs'.subset, htI⟩ -- Since `I` is contained in the supremum of `J` with the supremum of `s'`, -- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`. intro x hx diff --git a/Mathlib/Algebra/Ring/Subring/Defs.lean b/Mathlib/Algebra/Ring/Subring/Defs.lean index 31b88f1fa4d50..abae4f9c7f310 100644 --- a/Mathlib/Algebra/Ring/Subring/Defs.lean +++ b/Mathlib/Algebra/Ring/Subring/Defs.lean @@ -98,15 +98,16 @@ instance (priority := 75) toHasIntCast : IntCast s := -- Prefer subclasses of `Ring` over subclasses of `SubringClass`. /-- A subring of a ring inherits a ring structure -/ instance (priority := 75) toRing : Ring s := - Subtype.coe_injective.ring (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) + Subtype.coe_injective.ring Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl -- Prefer subclasses of `Ring` over subclasses of `SubringClass`. /-- A subring of a `CommRing` is a `CommRing`. -/ instance (priority := 75) toCommRing {R} [CommRing R] [SetLike S R] [SubringClass S R] : CommRing s := - Subtype.coe_injective.commRing (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) - (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl + Subtype.coe_injective.commRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) + (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) + (fun _ => rfl) fun _ => rfl -- Prefer subclasses of `Ring` over subclasses of `SubringClass`. /-- A subring of a domain is a domain. -/ diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean index b694e9070bc51..103afe35d71f9 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean @@ -294,7 +294,7 @@ lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb : #adaptation_note /-- 2024-11-10 added `(R := A)` -/ conv_rhs => rw [← sq_le_one_iff₀ (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self, star_mul, - IsSelfAdjoint.of_nonneg (R := A)sqrt_nonneg, IsSelfAdjoint.of_nonneg rpow_nonneg, + IsSelfAdjoint.of_nonneg (R := A) sqrt_nonneg, IsSelfAdjoint.of_nonneg rpow_nonneg, ← mul_assoc, mul_assoc _ _ (sqrt a), sqrt_mul_sqrt_self a, CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab] refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean index 79fd0dfe4e765..14fed41db183b 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean @@ -157,8 +157,14 @@ theorem cmp_dist_eq_cmp_dist_coe_center (z w : ℍ) (r : ℝ) : ((mul_neg_of_pos_of_neg w.im_pos (sinh_neg_iff.2 hr₀)).trans_le dist_nonneg).cmp_eq_gt.symm] have hr₀' : 0 ≤ w.im * Real.sinh r := by positivity have hzw₀ : 0 < 2 * z.im * w.im := by positivity - simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀, ← - (pow_left_strictMonoOn₀ two_ne_zero).cmp_map_eq dist_nonneg hr₀', dist_coe_center_sq] + #adaptation_note + /-- + After the bug fix in https://github.com/leanprover/lean4/pull/6024, + we need to give Lean the hint `(y := w.im * Real.sinh r)`. + -/ + simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀, + ← (pow_left_strictMonoOn₀ two_ne_zero).cmp_map_eq dist_nonneg (y := w.im * Real.sinh r) hr₀', + dist_coe_center_sq] rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add] theorem dist_eq_iff_dist_coe_center_eq : diff --git a/Mathlib/Data/DFinsupp/Sigma.lean b/Mathlib/Data/DFinsupp/Sigma.lean index 4df5f452d103f..6cfbbbe528a13 100644 --- a/Mathlib/Data/DFinsupp/Sigma.lean +++ b/Mathlib/Data/DFinsupp/Sigma.lean @@ -63,14 +63,14 @@ theorem sigmaCurry_zero [∀ i j, Zero (δ i j)] : @[simp] theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i : Σ _, _), δ i.1 i.2) : - sigmaCurry (f + g) = sigmaCurry f + sigmaCurry g := by + sigmaCurry (f + g) = (sigmaCurry f + sigmaCurry g : Π₀ (i) (j), δ i j) := by ext (i j) rfl @[simp] theorem sigmaCurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : Σ _, _), δ i.1 i.2) : - sigmaCurry (r • f) = r • sigmaCurry f := by + sigmaCurry (r • f) = (r • sigmaCurry f : Π₀ (i) (j), δ i j) := by ext (i j) rfl diff --git a/Mathlib/Data/Finset/Defs.lean b/Mathlib/Data/Finset/Defs.lean index a3260f4f702e4..70a17aa439250 100644 --- a/Mathlib/Data/Finset/Defs.lean +++ b/Mathlib/Data/Finset/Defs.lean @@ -213,6 +213,8 @@ instance partialOrder : PartialOrder (Finset α) where le_trans _ _ _ hst htu _ ha := htu <| hst ha le_antisymm _ _ hst hts := ext fun _ => ⟨@hst _, @hts _⟩ +theorem subset_of_le : s ≤ t → s ⊆ t := id + instance : IsRefl (Finset α) (· ⊆ ·) := show IsRefl (Finset α) (· ≤ ·) by infer_instance diff --git a/Mathlib/Data/Finset/SDiff.lean b/Mathlib/Data/Finset/SDiff.lean index 52b4f4ac894a3..1b6228553e58b 100644 --- a/Mathlib/Data/Finset/SDiff.lean +++ b/Mathlib/Data/Finset/SDiff.lean @@ -111,11 +111,11 @@ theorem sdiff_empty : s \ ∅ = s := @[mono, gcongr] theorem sdiff_subset_sdiff (hst : s ⊆ t) (hvu : v ⊆ u) : s \ u ⊆ t \ v := - sdiff_le_sdiff hst hvu + subset_of_le (sdiff_le_sdiff hst hvu) theorem sdiff_subset_sdiff_iff_subset {r : Finset α} (hs : s ⊆ r) (ht : t ⊆ r) : - r \ s ⊆ r \ t ↔ t ⊆ s := - sdiff_le_sdiff_iff_le hs ht + r \ s ⊆ r \ t ↔ t ⊆ s := by + simpa only [← le_eq_subset] using sdiff_le_sdiff_iff_le hs ht @[simp, norm_cast] theorem coe_sdiff (s₁ s₂ : Finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : Set α) := diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean index 9659c779dff54..ad4dbd36848f8 100644 --- a/Mathlib/Data/List/Sublists.lean +++ b/Mathlib/Data/List/Sublists.lean @@ -44,7 +44,7 @@ theorem sublists'Aux_eq_array_foldl (a : α) : ∀ (r₁ r₂ : List (List α)), sublists'Aux a r₁ r₂ = ((r₁.toArray).foldl (init := r₂.toArray) (fun r l => r.push (a :: l))).toList := by intro r₁ r₂ - rw [sublists'Aux, Array.foldl_eq_foldl_toList] + rw [sublists'Aux, Array.foldl_toList] have := List.foldl_hom Array.toList (fun r l => r.push (a :: l)) (fun r l => r ++ [a :: l]) r₁ r₂.toArray (by simp) simpa using this @@ -106,7 +106,7 @@ theorem sublistsAux_eq_array_foldl : (r.toArray.foldl (init := #[]) fun r l => (r.push l).push (a :: l)).toList := by funext a r - simp only [sublistsAux, Array.foldl_eq_foldl_toList, Array.mkEmpty] + simp only [sublistsAux, Array.foldl_toList, Array.mkEmpty] have := foldl_hom Array.toList (fun r l => (r.push l).push (a :: l)) (fun (r : List (List α)) l => r ++ [l, a :: l]) r #[] (by simp) @@ -127,7 +127,7 @@ theorem sublistsAux_eq_flatMap : ext α l : 2 trans l.foldr sublistsAux [[]] · rw [sublistsAux_eq_flatMap, sublists] - · simp only [sublistsFast, sublistsAux_eq_array_foldl, Array.foldr_eq_foldr_toList] + · simp only [sublistsFast, sublistsAux_eq_array_foldl, Array.foldr_toList] rw [← foldr_hom Array.toList] · intros _ _; congr diff --git a/Mathlib/FieldTheory/KummerExtension.lean b/Mathlib/FieldTheory/KummerExtension.lean index 273c7bd88310d..fee360c7fd681 100644 --- a/Mathlib/FieldTheory/KummerExtension.lean +++ b/Mathlib/FieldTheory/KummerExtension.lean @@ -425,7 +425,7 @@ def adjoinRootXPowSubCEquiv (hζ : (primitiveRoots n K).Nonempty) (H : Irreducib AlgEquiv.ofBijective (AdjoinRoot.liftHom (X ^ n - C a) α (by simp [hα])) <| by haveI := Fact.mk H letI := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H - refine ⟨(AlgHom.toRingHom _).injective, ?_⟩ + refine ⟨(liftHom (X ^ n - C a) α _).injective, ?_⟩ rw [← AlgHom.range_eq_top, ← IsSplittingField.adjoin_rootSet _ (X ^ n - C a), eq_comm, adjoin_rootSet_eq_range, IsSplittingField.adjoin_rootSet] exact IsSplittingField.splits _ _ diff --git a/Mathlib/FieldTheory/Relrank.lean b/Mathlib/FieldTheory/Relrank.lean index 6fe6ff6b4ca8b..abb53d55ae3a6 100644 --- a/Mathlib/FieldTheory/Relrank.lean +++ b/Mathlib/FieldTheory/Relrank.lean @@ -35,11 +35,13 @@ variable {E : Type v} [Field E] {L : Type w} [Field L] variable (A B C : Subfield E) +set_option synthInstance.maxHeartbeats 400000 in /-- `Subfield.relrank A B` is defined to be `[B : A ⊓ B]` as a `Cardinal`, in particular, when `A ≤ B` it is `[B : A]`, the degree of the field extension `B / A`. This is similar to `Subgroup.relindex` but it is `Cardinal` valued. -/ noncomputable def relrank := Module.rank ↥(A ⊓ B) (extendScalars (inf_le_right : A ⊓ B ≤ B)) +set_option synthInstance.maxHeartbeats 400000 in /-- The `Nat` version of `Subfield.relrank`. If `B / A ⊓ B` is an infinite extension, then it is zero. -/ noncomputable def relfinrank := finrank ↥(A ⊓ B) (extendScalars (inf_le_right : A ⊓ B ≤ B)) @@ -55,12 +57,14 @@ theorem relrank_eq_of_inf_eq (h : A ⊓ C = B ⊓ C) : relrank A C = relrank B C theorem relfinrank_eq_of_inf_eq (h : A ⊓ C = B ⊓ C) : relfinrank A C = relfinrank B C := congr(toNat $(relrank_eq_of_inf_eq h)) +set_option synthInstance.maxHeartbeats 400000 in /-- If `A ≤ B`, then `Subfield.relrank A B` is `[B : A]` -/ theorem relrank_eq_rank_of_le (h : A ≤ B) : relrank A B = Module.rank A (extendScalars h) := by rw [relrank] have := inf_of_le_left h congr! +set_option synthInstance.maxHeartbeats 400000 in /-- If `A ≤ B`, then `Subfield.relfinrank A B` is `[B : A]` -/ theorem relfinrank_eq_finrank_of_le (h : A ≤ B) : relfinrank A B = finrank A (extendScalars h) := congr(toNat $(relrank_eq_rank_of_le h)) @@ -112,6 +116,7 @@ theorem relrank_top_left : relrank ⊤ A = 1 := relrank_eq_one_of_le le_top @[simp] theorem relfinrank_top_left : relfinrank ⊤ A = 1 := relfinrank_eq_one_of_le le_top +set_option synthInstance.maxHeartbeats 400000 in @[simp] theorem relrank_top_right : relrank A ⊤ = Module.rank A E := by rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top, diff --git a/Mathlib/Geometry/Manifold/Instances/Real.lean b/Mathlib/Geometry/Manifold/Instances/Real.lean index 26caf2f7bee47..7871850496757 100644 --- a/Mathlib/Geometry/Manifold/Instances/Real.lean +++ b/Mathlib/Geometry/Manifold/Instances/Real.lean @@ -98,6 +98,7 @@ theorem interior_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) : change interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a rw [f.interior_preimage, interior_Ici] apply Function.surjective_eval + @[deprecated (since := "2024-11-12")] alias interior_halfspace := interior_halfSpace open ENNReal in @@ -108,6 +109,7 @@ theorem closure_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) : change closure (f ⁻¹' Ici a) = f ⁻¹' Ici a rw [f.closure_preimage, closure_Ici] apply Function.surjective_eval + @[deprecated (since := "2024-11-12")] alias closure_halfspace := closure_halfSpace open ENNReal in @@ -118,6 +120,7 @@ theorem closure_open_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) change closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a rw [f.closure_preimage, closure_Ioi] apply Function.surjective_eval + @[deprecated (since := "2024-11-12")] alias closure_open_halfspace := closure_open_halfSpace open ENNReal in diff --git a/Mathlib/GroupTheory/Congruence/Basic.lean b/Mathlib/GroupTheory/Congruence/Basic.lean index 2810c0bd2c101..91e24b00c44b1 100644 --- a/Mathlib/GroupTheory/Congruence/Basic.lean +++ b/Mathlib/GroupTheory/Congruence/Basic.lean @@ -256,7 +256,7 @@ lemma comapQuotientEquivOfSurj_symm_mk (c : Con M) {f : N →* M} (hf) (x : N) : MulEquiv function"] lemma comapQuotientEquivOfSurj_symm_mk' (c : Con M) (f : N ≃* M) (x : N) : ((@MulEquiv.symm (Con.Quotient (comap ⇑f _ c)) _ _ _ - (comapQuotientEquivOfSurj c f f.surjective)) ⟦f x⟧) = ↑x := + (comapQuotientEquivOfSurj c (f : N →* M) f.surjective)) ⟦f x⟧) = ↑x := (MulEquiv.symm_apply_eq (@comapQuotientEquivOfSurj M N _ _ c f _)).mpr rfl /-- The **second isomorphism theorem for monoids**. -/ diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index 4dd4c5369f2d3..eca3624e57fa4 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -764,7 +764,7 @@ nonrec theorem _root_.MulEquiv.isHaarMeasure_map [BorelSpace G] [TopologicalGrou [TopologicalGroup H] (e : G ≃* H) (he : Continuous e) (hesymm : Continuous e.symm) : IsHaarMeasure (Measure.map e μ) := let f : G ≃ₜ H := .mk e - isHaarMeasure_map μ e he e.surjective f.isClosedEmbedding.tendsto_cocompact + isHaarMeasure_map μ e.toMonoidHom he e.surjective f.isClosedEmbedding.tendsto_cocompact /-- A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map`. -/ instance _root_.ContinuousLinearEquiv.isAddHaarMeasure_map diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean b/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean index 62141d5c9d30c..9b017066d5c21 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean @@ -507,8 +507,10 @@ def arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α] [MeasurableS measurable_toFun _ h := by simp_rw [Equiv.arrowProdEquivProdArrow, coe_fn_mk] exact MeasurableSet.preimage h (Measurable.prod_mk - (measurable_pi_lambda (fun a c ↦ (a c).1) fun a ↦ (measurable_pi_apply a).fst) - (measurable_pi_lambda (fun a c ↦ (a c).2) fun a ↦ (measurable_pi_apply a).snd )) + (measurable_pi_lambda (fun (a : γ → α × β) c ↦ (a c).1) + fun a ↦ (measurable_pi_apply a).fst) + (measurable_pi_lambda (fun (a : γ → α × β) c ↦ (a c).2) + fun a ↦ (measurable_pi_apply a).snd)) measurable_invFun _ h := by simp_rw [Equiv.arrowProdEquivProdArrow, coe_fn_symm_mk] exact MeasurableSet.preimage h (by measurability) diff --git a/Mathlib/RingTheory/Jacobson.lean b/Mathlib/RingTheory/Jacobson.lean index 14e36f678fd84..960ec2b0a8e51 100644 --- a/Mathlib/RingTheory/Jacobson.lean +++ b/Mathlib/RingTheory/Jacobson.lean @@ -704,7 +704,7 @@ lemma finite_of_finite_type_of_isJacobsonRing (R S : Type*) [CommRing R] [Field obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_› have : (algebraMap R S).IsIntegral := by rw [← f.comp_algebraMap] - exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f hf + exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this exact Algebra.IsIntegral.finite diff --git a/Mathlib/RingTheory/Polynomial/UniqueFactorization.lean b/Mathlib/RingTheory/Polynomial/UniqueFactorization.lean index bf2b2308eda3b..36928dc10b7c6 100644 --- a/Mathlib/RingTheory/Polynomial/UniqueFactorization.lean +++ b/Mathlib/RingTheory/Polynomial/UniqueFactorization.lean @@ -125,7 +125,7 @@ instance (priority := 100) uniqueFactorizationMonoid : exact ⟨w.map (rename (↑)), fun b hb => let ⟨b', hb', he⟩ := Multiset.mem_map.1 hb - he ▸ (prime_rename_iff ↑s).2 (h b' hb'), + he ▸ (prime_rename_iff (σ := σ) ↑s).2 (h b' hb'), Units.map (@rename s σ D _ (↑)).toRingHom.toMonoidHom u, by erw [Multiset.prod_hom, ← map_mul, hw]⟩ diff --git a/lake-manifest.json b/lake-manifest.json index 3ec222bb45bf6..da3864d8e687d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ee6767b2157766c8aa451bb93d1434436e593a2", + "rev": "0fc755a2a762bd228db724df926de7d3e2306a34", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2b4fc3aa9ae06e749417a101d5a95de2c5e8b1b6", + "rev": "70fef96b919e8d032bbf6016cd284867d503d2d8", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "83b4115edfea21c2b9d3cc33742941ea1f9ba2e4", + "rev": "2ed85f320805f9d3a455ced3b181562ed146bc20", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index d6cb529aed891..97bb2ffae1c7e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-11-13 +leanprover/lean4:nightly-2024-11-14