From 4a97c893071433d0d39cbf5261d0877f864c2189 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 6 Feb 2025 11:31:11 +0100 Subject: [PATCH] chore: bump to stable `v4.16.0` (#337) --- FLT/AutomorphicRepresentation/Example.lean | 4 ++-- .../FiniteAdeleRing/BaseChange.lean | 8 ++----- FLT/GlobalLanglandsConjectures/GLnDefs.lean | 2 +- .../DistribHaarChar/RealComplex.lean | 4 ++-- FLT/MathlibExperiments/Coalgebra/Monoid.lean | 12 +++++----- .../Coalgebra/Sweedler.lean | 22 +++++++++---------- .../Coalgebra/TensorProduct.lean | 18 +++++++-------- FLT/MathlibExperiments/HopfAlgebra/Basic.lean | 16 +++++++------- FLT/MathlibExperiments/IsCentralSimple.lean | 2 +- docbuild/lakefile.toml | 2 +- lake-manifest.json | 8 +++---- lakefile.lean | 2 +- lean-toolchain | 2 +- 13 files changed, 49 insertions(+), 53 deletions(-) diff --git a/FLT/AutomorphicRepresentation/Example.lean b/FLT/AutomorphicRepresentation/Example.lean index db3cd451..6287529d 100644 --- a/FLT/AutomorphicRepresentation/Example.lean +++ b/FLT/AutomorphicRepresentation/Example.lean @@ -76,7 +76,7 @@ instance charZero : CharZero ZHat := ⟨ fun a b h ↦ by open BigOperators Nat Finset in /-- A nonarchimedean analogue `0! + 1! + 2! + ⋯` of `e = 1/0! + 1/1! + 1/2! + ⋯`. It is defined as the function whose value at `ZMod n` is the sum of `i!` for `0 ≤ i < n`.-/ -def e : ZHat := ⟨fun (n : ℕ+) ↦ ∑ i in range (n : ℕ), i !, by +def e : ZHat := ⟨fun (n : ℕ+) ↦ ∑ i ∈ range (n : ℕ), i !, by intros D N hDN dsimp only obtain ⟨k, hk⟩ := exists_add_of_le <| le_of_dvd N.pos hDN @@ -88,7 +88,7 @@ def e : ZHat := ⟨fun (n : ℕ+) ↦ ∑ i in range (n : ℕ), i !, by open BigOperators Nat Finset -lemma e_def (n : ℕ+) : e n = ∑ i in range (n : ℕ), (i ! : ZMod n) := rfl +lemma e_def (n : ℕ+) : e n = ∑ i ∈ range (n : ℕ), (i ! : ZMod n) := rfl lemma _root_.Nat.sum_factorial_lt_factorial_succ {j : ℕ} (hj : 1 < j) : ∑ i ∈ range (j + 1), i ! < (j + 1) ! := by diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index 4210372e..27146101 100644 --- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean +++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean @@ -342,9 +342,7 @@ theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi RingHom.coe_coe, AlgHom.coe_comp, AlgHom.coe_restrictScalars', AlgHom.coe_coe, Function.comp_apply, SetLike.mem_coe] induction' x with x y x y hx hy - · rw [(tensorAdicCompletionIntegersTo A K L B v).map_zero, - (tensorAdicCompletionComapAlgHom A K L B v).map_zero] - exact zero_mem _ + · simp [map_zero, Pi.zero_apply, zero_mem] · simp only [tensorAdicCompletionIntegersTo, Algebra.TensorProduct.lift_tmul, AlgHom.coe_comp, Function.comp_apply, Algebra.ofId_apply, AlgHom.commutes, Algebra.TensorProduct.algebraMap_apply, AlgHom.coe_restrictScalars', @@ -362,9 +360,7 @@ theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi · exact Ideal.IsDedekindDomain.ramificationIdx_ne_zero ((Ideal.map_eq_bot_iff_of_injective (algebraMap_injective_of_field_isFractionRing A B K L)).not.mpr (comap A i.1).3) i.1.2 Ideal.map_comap_le - · rw [(tensorAdicCompletionIntegersTo A K L B v).map_add, - (tensorAdicCompletionComapAlgHom A K L B v).map_add] - exact add_mem hx hy + · simp [map_add, Pi.add_apply, add_mem hx hy] theorem adicCompletionComapAlgEquiv_integral : ∃ S : Finset (HeightOneSpectrum A), ∀ v ∉ S, AlgHom.range (((tensorAdicCompletionComapAlgHom A K L B v).restrictScalars B).comp diff --git a/FLT/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean index 3fbd5368..5b6cef0d 100644 --- a/FLT/GlobalLanglandsConjectures/GLnDefs.lean +++ b/FLT/GlobalLanglandsConjectures/GLnDefs.lean @@ -284,7 +284,7 @@ open CategoryTheory noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) : FDRep ℂ (orthogonalGroup (Fin n) ℝ) where V := FGModuleCat.of ℂ (Fin w.d → ℂ) - ρ := { + ρ := MonCat.ofHom { toFun := fun A ↦ ModuleCat.ofHom { toFun := fun x ↦ (w.rho A).1 *ᵥ x map_add' := fun _ _ ↦ Matrix.mulVec_add .. diff --git a/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean b/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean index 748094f2..1e987e68 100644 --- a/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean +++ b/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean @@ -31,7 +31,7 @@ open Real Complex MeasureTheory Measure Set open scoped Pointwise lemma Real.volume_real_smul (x : ℝ) (s : Set ℝ) : volume (x • s) = ‖x‖₊ * volume s := by - simp [← ennnorm_eq_ofReal_abs] + simp [← enorm_eq_ofReal_abs, enorm_eq_nnnorm] /-- The distributive Haar character of the action of `ℝˣ` on `ℝ` is the usual norm. @@ -62,7 +62,7 @@ lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ) (f := (LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ) _ _ using 2 · simpa [LinearMap.mul, LinearMap.mk₂, LinearMap.mk₂', LinearMap.mk₂'ₛₗ, Units.smul_def, eq_comm] using preimage_smul_inv z (Icc 0 1 ×ℂ Icc 0 1) - · simp [key, ofReal_norm_eq_coe_nnnorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat] + · simp [key, ofReal_norm_eq_enorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat]; rfl · simp [key, zpow_ofNat] lemma Complex.volume_complex_smul (z : ℂ) (s : Set ℂ) : volume (z • s) = ‖z‖₊ ^ 2 * volume s := by diff --git a/FLT/MathlibExperiments/Coalgebra/Monoid.lean b/FLT/MathlibExperiments/Coalgebra/Monoid.lean index 6f833a5a..4e975c73 100644 --- a/FLT/MathlibExperiments/Coalgebra/Monoid.lean +++ b/FLT/MathlibExperiments/Coalgebra/Monoid.lean @@ -68,13 +68,13 @@ lemma mul_def (φ ψ : LinearPoint R A L) : φ * ψ = LinearMap.mul' _ _ ∘ₗ TensorProduct.map φ ψ ∘ₗ Coalgebra.comul := rfl lemma mul_repr' {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) - (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) : - φ.mul ψ a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := by + (repr : Coalgebra.comul (R := R) a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ Δ₂ i) : + φ.mul ψ a = ∑ i ∈ ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := by simp only [mul, comp_apply, repr, map_sum, map_tmul, mul'_apply] lemma mul_repr {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) - (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) : - (φ * ψ) a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := + (repr : Coalgebra.comul (R := R) a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ Δ₂ i) : + (φ * ψ) a = ∑ i ∈ ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := mul_repr' _ _ a ℐ Δ₁ Δ₂ repr lemma mul_assoc' : φ * ψ * χ = φ * (ψ * χ) := LinearMap.ext fun x ↦ by @@ -172,8 +172,8 @@ lemma mul_def (φ ψ : AlgHomPoint R A L) : Algebra.TensorProduct.map φ ψ |>.comp <| Bialgebra.comulAlgHom R A) := rfl lemma mul_repr {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) - (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) : - (φ * ψ) a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := + (repr : Coalgebra.comul (R := R) a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ Δ₂ i) : + (φ * ψ) a = ∑ i ∈ ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := LinearPoint.mul_repr _ _ a ℐ Δ₁ Δ₂ repr lemma mul_assoc' : φ * ψ * χ = φ * (ψ * χ) := by diff --git a/FLT/MathlibExperiments/Coalgebra/Sweedler.lean b/FLT/MathlibExperiments/Coalgebra/Sweedler.lean index ec696374..7a235633 100644 --- a/FLT/MathlibExperiments/Coalgebra/Sweedler.lean +++ b/FLT/MathlibExperiments/Coalgebra/Sweedler.lean @@ -31,18 +31,18 @@ variable [AddCommMonoid A] [Module R A] [Coalgebra R A] lemma exists_repr (x : A) : ∃ (I : Finset (A ⊗[R] A)) (x1 : A ⊗[R] A → A) (x2 : A ⊗[R] A → A), - Coalgebra.comul x = ∑ i in I, x1 i ⊗ₜ[R] x2 i := by + Coalgebra.comul x = ∑ i ∈ I, x1 i ⊗ₜ[R] x2 i := by classical have mem1 : comul x ∈ (⊤ : Submodule R (A ⊗[R] A)) := ⟨⟩ rw [← TensorProduct.span_tmul_eq_top, mem_span_set] at mem1 - obtain ⟨r, hr, (eq1 : ∑ i in r.support, (_ • _) = _)⟩ := mem1 + obtain ⟨r, hr, (eq1 : ∑ i ∈ r.support, (_ • _) = _)⟩ := mem1 choose a a' haa' using hr replace eq1 := calc _ - comul x = ∑ i in r.support, r i • i := eq1.symm - _ = ∑ i in r.support.attach, (r i : R) • i.1 := Finset.sum_attach _ _ |>.symm - _ = ∑ i in r.support.attach, (r i • a i.2 ⊗ₜ[R] a' i.2) := + comul x = ∑ i ∈ r.support, r i • i := eq1.symm + _ = ∑ i ∈ r.support.attach, (r i : R) • i.1 := Finset.sum_attach _ _ |>.symm + _ = ∑ i ∈ r.support.attach, (r i • a i.2 ⊗ₜ[R] a' i.2) := Finset.sum_congr rfl fun i _ ↦ congr(r i.1 • $(haa' i.2)).symm - _ = ∑ i in r.support.attach, ((r i • a i.2) ⊗ₜ[R] a' i.2) := + _ = ∑ i ∈ r.support.attach, ((r i • a i.2) ⊗ₜ[R] a' i.2) := Finset.sum_congr rfl fun i _ ↦ TensorProduct.smul_tmul' _ _ _ refine ⟨r.support, fun i ↦ if h : i ∈ r.support then r i • a h else 0, fun i ↦ if h : i ∈ r.support then a' h else 0, eq1 ▸ ?_⟩ @@ -60,17 +60,17 @@ noncomputable def Δ₂ (a : A) : A ⊗[R] A → A := exists_repr a |>.choose_spec.choose_spec.choose lemma comul_repr (a : A) : - Coalgebra.comul a = ∑ i in ℐ a, Δ₁ a i ⊗ₜ[R] Δ₂ (R := R) a i := + Coalgebra.comul a = ∑ i ∈ ℐ a, Δ₁ a i ⊗ₜ[R] Δ₂ (R := R) a i := exists_repr a |>.choose_spec.choose_spec.choose_spec lemma sum_counit_tmul (a : A) {ι : Type*} (s : Finset ι) (x y : ι → A) - (repr : comul a = ∑ i in s, x i ⊗ₜ[R] y i) : - ∑ i in s, counit (R := R) (x i) ⊗ₜ y i = 1 ⊗ₜ[R] a := by + (repr : comul a = ∑ i ∈ s, x i ⊗ₜ[R] y i) : + ∑ i ∈ s, counit (R := R) (x i) ⊗ₜ y i = 1 ⊗ₜ[R] a := by simpa [repr, map_sum] using congr($(rTensor_counit_comp_comul (R := R) (A := A)) a) lemma sum_tmul_counit (a : A) {ι : Type*} (s : Finset ι) (x y : ι → A) - (repr : comul a = ∑ i in s, x i ⊗ₜ[R] y i) : - ∑ i in s, (x i) ⊗ₜ counit (R := R) (y i) = a ⊗ₜ[R] 1 := by + (repr : comul a = ∑ i ∈ s, x i ⊗ₜ[R] y i) : + ∑ i ∈ s, (x i) ⊗ₜ counit (R := R) (y i) = a ⊗ₜ[R] 1 := by simpa [repr, map_sum] using congr($(lTensor_counit_comp_comul (R := R) (A := A)) a) end Coalgebra diff --git a/FLT/MathlibExperiments/Coalgebra/TensorProduct.lean b/FLT/MathlibExperiments/Coalgebra/TensorProduct.lean index 6e7ccb0a..ef79e8eb 100644 --- a/FLT/MathlibExperiments/Coalgebra/TensorProduct.lean +++ b/FLT/MathlibExperiments/Coalgebra/TensorProduct.lean @@ -94,23 +94,23 @@ variable {R A B} lemma comul_apply_repr (a : A) (b : B) {ιA ιB : Type*} (sA : Finset ιA) (sB : Finset ιB) - (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i) - (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) : - comul (a ⊗ₜ[R] b) = ∑ i in sA, ∑ j in sB, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by + (xA yA : ιA → A) (repr_a : comul a = ∑ i ∈ sA, xA i ⊗ₜ[R] yA i) + (xB yB : ιB → B) (repr_b : comul b = ∑ i ∈ sB, xB i ⊗ₜ[R] yB i) : + comul (a ⊗ₜ[R] b) = ∑ i ∈ sA, ∑ j ∈ sB, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by simpa [TensorProduct.comul_def, repr_a, repr_b, map_sum, sum_tmul, tmul_sum] using Finset.sum_comm lemma comul_apply_repr' (a : A) (b : B) {ιA ιB : Type*} (sA : Finset ιA) (sB : Finset ιB) - (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i) - (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) : - comul (a ⊗ₜ[R] b) = ∑ j in sB, ∑ i in sA, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by + (xA yA : ιA → A) (repr_a : comul a = ∑ i ∈ sA, xA i ⊗ₜ[R] yA i) + (xB yB : ιB → B) (repr_b : comul b = ∑ i ∈ sB, xB i ⊗ₜ[R] yB i) : + comul (a ⊗ₜ[R] b) = ∑ j ∈ sB, ∑ i ∈ sA, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by simp [TensorProduct.comul_def, repr_a, repr_b, map_sum, sum_tmul, tmul_sum] lemma comul_apply_repr'' (a : A) (b : B) {ιA ιB : Type*} (sA : Finset ιA) (sB : Finset ιB) - (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i) - (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) : - comul (a ⊗ₜ[R] b) = ∑ i in sA ×ˢ sB, (xA i.1 ⊗ₜ xB i.2) ⊗ₜ[R] (yA i.1 ⊗ₜ yB i.2) := by + (xA yA : ιA → A) (repr_a : comul a = ∑ i ∈ sA, xA i ⊗ₜ[R] yA i) + (xB yB : ιB → B) (repr_b : comul b = ∑ i ∈ sB, xB i ⊗ₜ[R] yB i) : + comul (a ⊗ₜ[R] b) = ∑ i ∈ sA ×ˢ sB, (xA i.1 ⊗ₜ xB i.2) ⊗ₜ[R] (yA i.1 ⊗ₜ yB i.2) := by rw [TensorProduct.comul_apply_repr (repr_a := repr_a) (repr_b := repr_b), Finset.sum_product] end Coalgebra diff --git a/FLT/MathlibExperiments/HopfAlgebra/Basic.lean b/FLT/MathlibExperiments/HopfAlgebra/Basic.lean index fd222c98..d56031bf 100644 --- a/FLT/MathlibExperiments/HopfAlgebra/Basic.lean +++ b/FLT/MathlibExperiments/HopfAlgebra/Basic.lean @@ -36,27 +36,27 @@ variable (A : Type*) [Semiring A] [HopfAlgebra R A] variable {R A} lemma antipode_repr {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) - (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : - ∑ i in ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = algebraMap R A (Coalgebra.counit a) := by + (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i ∈ ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = algebraMap R A (Coalgebra.counit a) := by have := mul_antipode_rTensor_comul_apply (R := R) a rw [repr, map_sum, map_sum] at this exact this lemma antipode_repr_eq_smul {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) - (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : - ∑ i in ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = (Coalgebra.counit a : R) • (1 : A) := by + (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i ∈ ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = (Coalgebra.counit a : R) • (1 : A) := by rw [antipode_repr (repr := repr), Algebra.smul_def, mul_one] lemma antipode_repr' {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) - (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : - ∑ i in ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = algebraMap R A (Coalgebra.counit a) := by + (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i ∈ ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = algebraMap R A (Coalgebra.counit a) := by have := mul_antipode_lTensor_comul_apply (R := R) a rw [repr, map_sum, map_sum] at this exact this lemma antipode_repr_eq_smul' {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) - (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : - ∑ i in ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = (Coalgebra.counit a : R) • 1 := by + (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i ∈ ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = (Coalgebra.counit a : R) • 1 := by rw [antipode_repr' (repr := repr), Algebra.smul_def, mul_one] lemma antipode_mul_id : antipode (R := R) (A := A) * LinearMap.id = 1 := by diff --git a/FLT/MathlibExperiments/IsCentralSimple.lean b/FLT/MathlibExperiments/IsCentralSimple.lean index 38acbbaf..0e473b98 100644 --- a/FLT/MathlibExperiments/IsCentralSimple.lean +++ b/FLT/MathlibExperiments/IsCentralSimple.lean @@ -35,7 +35,7 @@ structure IsCentralSimple variable (K : Type u) [Field K] theorem RingCon.sum {R : Type u} [AddCommMonoid R] [Mul R] {ι : Type v} {s : Finset ι} {a b : ι → R} - {r : RingCon R} (h : ∀ i ∈ s, r (a i) (b i)) : r (∑ i in s, a i) (∑ i in s, b i) := by + {r : RingCon R} (h : ∀ i ∈ s, r (a i) (b i)) : r (∑ i ∈ s, a i) (∑ i ∈ s, b i) := by induction s using Finset.induction_on with | empty => simp only [Finset.sum_empty] diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml index 127b04bd..463d142d 100644 --- a/docbuild/lakefile.toml +++ b/docbuild/lakefile.toml @@ -10,4 +10,4 @@ path = "../" [[require]] scope = "leanprover" name = "doc-gen4" -rev = "main" +rev = "v4.16.0" diff --git a/lake-manifest.json b/lake-manifest.json index 7396fd73..90cbae7e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2a71f56e8867536abeae5d73fdb6666dc21ff7d4", + "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "stable", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f72319c9686788305a8ab059f3c4d8c724785c83", + "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d", + "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index 82a58e1c..d14367d7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ package FLT where ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit ] -require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "master" +require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "stable" require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" diff --git a/lean-toolchain b/lean-toolchain index 2ffc30ce..8b4f470c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.16.0-rc2 \ No newline at end of file +leanprover/lean4:v4.16.0 \ No newline at end of file