chore: bump mathlib to 3069656, fix breaking changes

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]
 

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} ⊆

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

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",

lakefile.toml

@@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "169c26b52a38b704fad2c009372d76844a059bdf"
+rev = "30696563acb0596ab44d272bc5dfee96b2e72263"
 
 [[lean_lib]]
 name = "Cslib"