From b34f6d0bf880b2c8774aef9ac3b953ffb06e8c07 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Thu, 30 Jul 2026 20:32:53 +0000 Subject: [PATCH 1/3] chore: bump mathlib to 3069656: feat: `haveI`/`letI` tactic linter (#41657) (2026-07-29) --- lake-manifest.json | 6 +++--- lakefile.toml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7f68c0042..d1fe8e8d4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "169c26b52a38b704fad2c009372d76844a059bdf", + "rev": "30696563acb0596ab44d272bc5dfee96b2e72263", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "169c26b52a38b704fad2c009372d76844a059bdf", + "inputRev": "30696563acb0596ab44d272bc5dfee96b2e72263", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366", + "rev": "d60e6444e6fd881dfa077ff36e96de75753afa28", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index a1fe432a2..80a7caac4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "169c26b52a38b704fad2c009372d76844a059bdf" +rev = "30696563acb0596ab44d272bc5dfee96b2e72263" [[lean_lib]] name = "Cslib" From 012c46b6f58120fcf9eff2be7f4977d054ac2f33 Mon Sep 17 00:00:00 2001 From: Joscha Date: Mon, 3 Aug 2026 20:07:41 +0200 Subject: [PATCH 2/3] fix lints? --- Cslib/Foundations/Semantics/LTS/Termination.lean | 4 ++-- Cslib/MachineLearning/PACLearning/VersionSpace.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Termination.lean b/Cslib/Foundations/Semantics/LTS/Termination.lean index 9f3e4184c..6d72fe5ce 100644 --- a/Cslib/Foundations/Semantics/LTS/Termination.lean +++ b/Cslib/Foundations/Semantics/LTS/Termination.lean @@ -63,13 +63,13 @@ states. -/ theorem Acyclic.toBoundedUpTo [Finite State] (h : lts.Acyclic) : lts.BoundedUpTo (Nat.card State) := by classical - letI := Fintype.ofFinite State + let := Fintype.ofFinite State rw [Nat.card_eq_fintype_card] intro s1 μs s2 hmtr obtain ⟨states, hexec⟩ := Execution.of_mTr hmtr have hchain : states.IsChain (Relation.TransGen lts.UnlabelledTr) := hexec.isChain.imp_of_mem_imp fun _ _ _ _ htr => .single htr - letI : Std.Irrefl (Relation.TransGen lts.UnlabelledTr) := h.acyclic + let : Std.Irrefl (Relation.TransGen lts.UnlabelledTr) := h.acyclic have hcard := hchain.pairwise.nodup.length_le_card grind [Execution] diff --git a/Cslib/MachineLearning/PACLearning/VersionSpace.lean b/Cslib/MachineLearning/PACLearning/VersionSpace.lean index ee8a7c9c2..f3989e345 100644 --- a/Cslib/MachineLearning/PACLearning/VersionSpace.lean +++ b/Cslib/MachineLearning/PACLearning/VersionSpace.lean @@ -252,7 +252,7 @@ private lemma pi_map_graph_eq_one (Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x)))) (Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1})) = 1 := by have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop - haveI : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := + have : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := Measure.isProbabilityMeasure_map hφ.aemeasurable rw [Measure.pi_pi] simp [map_graph_eq_one hcm P hG] @@ -269,7 +269,7 @@ theorem ae_mem_versionSpace_of_realizable ∂(Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x)))), c ∈ VersionSpace C S := by have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop - haveI : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := + have : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := Measure.isProbabilityMeasure_map hφ.aemeasurable rw [ae_iff] have hsub : {S : Fin m → α × β | ¬ c ∈ VersionSpace C S} ⊆ From e8337a1af3e83109fa47dc123e74194d5068d123 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 3 Aug 2026 20:23:29 +0100 Subject: [PATCH 3/3] linter in tests --- CslibTests/Modal.lean | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/CslibTests/Modal.lean b/CslibTests/Modal.lean index 002acd9bf..be9f5b880 100644 --- a/CslibTests/Modal.lean +++ b/CslibTests/Modal.lean @@ -17,62 +17,62 @@ variable {World Atom : Type*} {φ : Proposition Atom} example : ((◇◇φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ K45 World Atom := by intro m h w - letI : IsTrans World m.r := h.1 - letI : Relation.RightEuclidean m.r := h.2 + let : IsTrans World m.r := h.1 + let : Relation.RightEuclidean m.r := h.2 exact ⟨Satisfies.four φ, Satisfies.five φ⟩ example : ((□φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ D4 World Atom := by intro m h w - letI : Relation.Serial m.r := h.1 - letI : IsTrans World m.r := h.2 + let : Relation.Serial m.r := h.1 + let : IsTrans World m.r := h.2 exact ⟨Satisfies.d φ, Satisfies.four φ⟩ example : ((□φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ D5 World Atom := by intro m h w - letI : Relation.Serial m.r := h.1 - letI : Relation.RightEuclidean m.r := h.2 + let : Relation.Serial m.r := h.1 + let : Relation.RightEuclidean m.r := h.2 exact ⟨Satisfies.d φ, Satisfies.five φ⟩ example : Proposition.and (□φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈ D45 World Atom := by intro m h w - letI : Relation.Serial m.r := h.1 - letI : IsTrans World m.r := h.2.1 - letI : Relation.RightEuclidean m.r := h.2.2 + let : Relation.Serial m.r := h.1 + let : IsTrans World m.r := h.2.1 + let : Relation.RightEuclidean m.r := h.2.2 exact ⟨Satisfies.d φ, Satisfies.four φ, Satisfies.five φ⟩ example : ((□φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ DB World Atom := by intro m h w - letI : Relation.Serial m.r := h.1 - letI : Std.Symm m.r := h.2 + let : Relation.Serial m.r := h.1 + let : Std.Symm m.r := h.2 exact ⟨Satisfies.d φ, Satisfies.b φ⟩ example : ((φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ TB World Atom := by intro m h w - letI : Std.Refl m.r := h.1 - letI : Std.Symm m.r := h.2 + let : Std.Refl m.r := h.1 + let : Std.Symm m.r := h.2 exact ⟨Satisfies.t φ, Satisfies.b φ⟩ example : ((φ → □◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ KB5 World Atom := by intro m h w - letI : Std.Symm m.r := h.1 - letI : Relation.RightEuclidean m.r := h.2 + let : Std.Symm m.r := h.1 + let : Relation.RightEuclidean m.r := h.2 exact ⟨Satisfies.b φ, Satisfies.five φ⟩ example : ((φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ S4 World Atom := by intro m h w - letI : Std.Refl m.r := h.1 - letI : IsTrans World m.r := h.2 + let : Std.Refl m.r := h.1 + let : IsTrans World m.r := h.2 exact ⟨Satisfies.t φ, Satisfies.four φ⟩ example : Proposition.and (φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈ S5 World Atom := by intro m h w - letI : Std.Refl m.r := h.1 - letI : IsTrans World m.r := h.2.1 - letI : Relation.RightEuclidean m.r := h.2.2 + let : Std.Refl m.r := h.1 + let : IsTrans World m.r := h.2.1 + let : Relation.RightEuclidean m.r := h.2.2 exact ⟨Satisfies.t φ, Satisfies.four φ, Satisfies.five φ⟩ end Cslib.Logic.Modal