chore: bump toolchain to v4.31.0-rc1 (#609)

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Co-authored-by: Alexandre Rademaker <arademaker@gmail.com>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>

Author: 10 people

Cslib.lean

@@ -1,4 +1,4 @@
-module  -- shake: keep-all
+module  -- shake: keep-all --deprecated_module: ignore
 
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM

Cslib/Computability/Automata/DA/Congr.lean

@@ -62,7 +62,7 @@ theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a})
   /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
   constructor <;>
   · intro h
-    simpa [mem_language, Accepts, congr_mtr_eq] using h
+    simpa [mem_language, Accepts, congr_mtr_eq] using! h
 
 end FinAcc
 

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -142,7 +142,7 @@ theorem buchiFamily_cover [Inhabited Symbol] [Finite State] :
       simp_all only [extract_drop, color]
       split_ifs with h
       · have : f k ≤ f (k + 1) := by lia
-        have : f 0 + (f k - f 0) = f k := by lia
+        have : f 0 + (f k - f 0) = f k := by grind
         have : f 0 + (f (k + 1) - f 0) = f (k + 1) := by lia
         simp_all
         rfl

Cslib/Computability/Machines/SingleTapeTuring/Basic.lean

@@ -384,8 +384,6 @@ This section defines the notion of time-bounded Turing Machines
 
 section TimeComputable
 
-variable [Inhabited Symbol] [Fintype Symbol]
-
 /-- A Turing machine + a time function +
 a proof it outputs `f` in at most `time(input.length)` steps. -/
 structure TimeComputable (f : List Symbol → List Symbol) where
@@ -470,8 +468,6 @@ section PolyTimeComputable
 
 open Polynomial
 
-variable [Inhabited Symbol] [Fintype Symbol]
-
 /-- A Turing machine + a polynomial time function +
 a proof it outputs `f` in at most `time(input.length)` steps. -/
 structure PolyTimeComputable (f : List Symbol → List Symbol) extends TimeComputable f where

Cslib/Crypto/Protocols/SecretSharing/Shamir.lean

@@ -153,7 +153,7 @@ private theorem privacyCorrectionPolynomial_eval
     (privacyCorrectionPolynomial (F := F) params s secret₀ secret₁).eval (params.point i) =
       (secret₀ - secret₁) / params.point i := by
   classical
-  simpa using
+  simpa using!
     (_root_.Lagrange.eval_interpolate_at_node
       (s := s.attach)
       (v := fun j : s => params.point j)

Cslib/Foundations/Control/Monad/Free.lean

@@ -230,7 +230,8 @@ lemma liftM_lift_bind (interp : {ι : Type u} → F ι → m ι) (op : F β) (co
 @[simp]
 lemma liftM_lift [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (op : F β) :
     (lift op).liftM interp = interp op := by
-  simp_rw [lift, FreeM.liftM, _root_.bind_pure]
+  rw [lift, FreeM.liftM]
+  simp
 
 @[simp]
 lemma liftM_bind [LawfulMonad m]

Cslib/Foundations/Control/Monad/Free/Effects.lean

@@ -449,7 +449,7 @@ instance instMonadWithReaderOf : MonadWithReaderOf σ (FreeReader σ) where
   | pure a => rfl
   | liftBind op cont ih =>
     cases op
-    simpa [withTheReader, instMonadWithReaderOf, run] using (ih (f s) s)
+    simpa [withTheReader, instMonadWithReaderOf, run] using! (ih (f s) s)
 
 end FreeReader
 

Cslib/Foundations/Data/HasFresh.lean

@@ -8,16 +8,17 @@ module -- shake: keep-downstream
 
 public import Cslib.Init
 public import Mathlib.Analysis.Normed.Field.Lemmas
+meta import Lean.Elab.ConfigEval
 import Qq
 
 /-! Computable chacterization of infinite types. -/
 
+namespace Cslib
+
 @[expose] public section
 
 universe u
 
-namespace Cslib
-
 /-- A type `α` has a computable `fresh` function if it is always possible, for any finite set
 of `α`, to compute a fresh element not in the set. -/
 class HasFresh (α : Type u) where
@@ -33,6 +34,63 @@ in proofs. -/
 theorem HasFresh.fresh_exists {α : Type u} [HasFresh α] (s : Finset α) : ∃ a, a ∉ s :=
   ⟨fresh s, fresh_notMem s⟩
 
+export HasFresh (fresh fresh_notMem fresh_exists)
+
+/-- `HasFresh α` implies a computably infinite type. -/
+instance HasFresh.to_infinite (α : Type u) [HasFresh α] : Infinite α := by
+  apply Infinite.of_not_fintype
+  rintro ⟨elems, _⟩
+  grind [fresh_notMem elems]
+
+/-- All infinite types have an associated (at least noncomputable) fresh function.
+This, in conjunction with `HasFresh.to_infinite`, characterizes `HasFresh`. -/
+noncomputable instance (α : Type u) [Infinite α] : HasFresh α where
+  fresh s := Infinite.exists_notMem_finset s |>.choose
+  fresh_notMem s := by grind
+
+open Finset in
+/-- Construct a fresh element from an embedding of `ℕ` using `Nat.find`. -/
+@[implicit_reducible]
+def HasFresh.ofNatEmbed {α : Type u} [DecidableEq α] (e : ℕ ↪ α) : HasFresh α where
+  fresh s := e (Nat.find (p := fun n ↦ e n ∉ s) ⟨(s.preimage e e.2.injOn).max.succ,
+    fun h ↦ not_lt_of_ge (le_max <| mem_preimage.2 h) (WithBot.lt_succ _)⟩)
+  fresh_notMem s := Nat.find_spec (p := fun n ↦ e n ∉ s) _
+
+/-- Construct a fresh element given a function `f` with `x < f x`. -/
+@[implicit_reducible]
+def HasFresh.ofSucc {α : Type u} [Inhabited α] [SemilatticeSup α] (f : α → α) (hf : ∀ x, x < f x) :
+    HasFresh α where
+  fresh s := if hs : s.Nonempty then f (s.sup' hs id) else default
+  fresh_notMem s h := if hs : s.Nonempty
+    then not_le_of_gt (hf (s.sup' hs id)) <| by rw [dif_pos hs] at h; exact s.le_sup' id h
+    else hs ⟨_, h⟩
+
+/-- `ℕ` has a computable fresh function. -/
+instance : HasFresh ℕ :=
+  .ofSucc (· + 1) Nat.lt_add_one
+
+/-- `ℤ` has a computable fresh function. -/
+instance : HasFresh ℤ :=
+  .ofSucc (· + 1) Int.lt_succ
+
+/-- `ℚ` has a computable fresh function. -/
+instance : HasFresh ℚ :=
+  .ofSucc (· + 1) fun x ↦ lt_add_of_pos_right x one_pos
+
+/-- If `α` has a computable fresh function, then so does `Finset α`. -/
+instance {α : Type u} [DecidableEq α] [HasFresh α] : HasFresh (Finset α) :=
+  .ofSucc (fun s ↦ insert (fresh s) s) fun s ↦ Finset.ssubset_insert <| fresh_notMem s
+
+/-- If `α` is inhabited, then `Multiset α` has a computable fresh function. -/
+instance {α : Type u} [DecidableEq α] [Inhabited α] : HasFresh (Multiset α) :=
+  .ofSucc (fun s ↦ default ::ₘ s) fun _ ↦ Multiset.lt_cons_self _ _
+
+/-- `ℕ → ℕ` has a computable fresh function. -/
+instance : HasFresh (ℕ → ℕ) :=
+  .ofSucc (fun f x ↦ f x + 1) fun _ ↦ Pi.lt_def.2 ⟨fun _ ↦ Nat.le_succ _, 0, Nat.lt_succ_self _⟩
+
+end
+
 public meta section
 
 open Lean Elab Term Meta Parser Tactic
@@ -45,7 +103,7 @@ structure FreeUnionConfig where
   finset : Bool := true
 
 /-- Elaborate a FreeUnionConfig. -/
-declare_config_elab elabFreeUnionConfig FreeUnionConfig
+declare_term_config_elab elabFreeUnionConfig FreeUnionConfig
 
 /--
   Given a `DecidableEq Var` instance, this elaborator automatically constructs
@@ -87,7 +145,7 @@ set_option linter.style.emptyLine false in
 def HasFresh.freeUnion : TermElab := fun stx _ => do
   match stx with
   | `(free_union $cfg $[[$maps,*]]? $var:term) =>
-    let cfg ← elabFreeUnionConfig cfg |>.run { elaborator := .anonymous } |>.run' { goals := [] }
+    let cfg ← elabFreeUnionConfig cfg
 
     -- the type of our variables
     let var ← elabType var
@@ -124,59 +182,4 @@ def HasFresh.freeUnion : TermElab := fun stx _ => do
 
 end
 
-export HasFresh (fresh fresh_notMem fresh_exists)
-
-/-- `HasFresh α` implies a computably infinite type. -/
-instance HasFresh.to_infinite (α : Type u) [HasFresh α] : Infinite α := by
-  apply Infinite.of_not_fintype
-  rintro ⟨elems, _⟩
-  grind [fresh_notMem elems]
-
-/-- All infinite types have an associated (at least noncomputable) fresh function.
-This, in conjunction with `HasFresh.to_infinite`, characterizes `HasFresh`. -/
-noncomputable instance (α : Type u) [Infinite α] : HasFresh α where
-  fresh s := Infinite.exists_notMem_finset s |>.choose
-  fresh_notMem s := by grind
-
-open Finset in
-/-- Construct a fresh element from an embedding of `ℕ` using `Nat.find`. -/
-@[implicit_reducible]
-def HasFresh.ofNatEmbed {α : Type u} [DecidableEq α] (e : ℕ ↪ α) : HasFresh α where
-  fresh s := e (Nat.find (p := fun n ↦ e n ∉ s) ⟨(s.preimage e e.2.injOn).max.succ,
-    fun h ↦ not_lt_of_ge (le_max <| mem_preimage.2 h) (WithBot.lt_succ _)⟩)
-  fresh_notMem s := Nat.find_spec (p := fun n ↦ e n ∉ s) _
-
-/-- Construct a fresh element given a function `f` with `x < f x`. -/
-@[implicit_reducible]
-def HasFresh.ofSucc {α : Type u} [Inhabited α] [SemilatticeSup α] (f : α → α) (hf : ∀ x, x < f x) :
-    HasFresh α where
-  fresh s := if hs : s.Nonempty then f (s.sup' hs id) else default
-  fresh_notMem s h := if hs : s.Nonempty
-    then not_le_of_gt (hf (s.sup' hs id)) <| by rw [dif_pos hs] at h; exact s.le_sup' id h
-    else hs ⟨_, h⟩
-
-/-- `ℕ` has a computable fresh function. -/
-instance : HasFresh ℕ :=
-  .ofSucc (· + 1) Nat.lt_add_one
-
-/-- `ℤ` has a computable fresh function. -/
-instance : HasFresh ℤ :=
-  .ofSucc (· + 1) Int.lt_succ
-
-/-- `ℚ` has a computable fresh function. -/
-instance : HasFresh ℚ :=
-  .ofSucc (· + 1) fun x ↦ lt_add_of_pos_right x one_pos
-
-/-- If `α` has a computable fresh function, then so does `Finset α`. -/
-instance {α : Type u} [DecidableEq α] [HasFresh α] : HasFresh (Finset α) :=
-  .ofSucc (fun s ↦ insert (fresh s) s) fun s ↦ Finset.ssubset_insert <| fresh_notMem s
-
-/-- If `α` is inhabited, then `Multiset α` has a computable fresh function. -/
-instance {α : Type u} [DecidableEq α] [Inhabited α] : HasFresh (Multiset α) :=
-  .ofSucc (fun s ↦ default ::ₘ s) fun _ ↦ Multiset.lt_cons_self _ _
-
-/-- `ℕ → ℕ` has a computable fresh function. -/
-instance : HasFresh (ℕ → ℕ) :=
-  .ofSucc (fun f x ↦ f x + 1) fun _ ↦ Pi.lt_def.2 ⟨fun _ ↦ Nat.le_succ _, 0, Nat.lt_succ_self _⟩
-
 end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean

@@ -75,14 +75,14 @@ set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- Any typable term either has a reduction step or is a value. -/
 lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' := by
   generalize eq : [] = Γ at der
-  have der' : Typing Γ t τ := by assumption
-  induction der <;> subst eq <;> simp only [forall_const] at *
+  have der' : Typing Γ t τ := der
+  induction der <;> subst eq
   case var mem => grind
   case app t₁ _ _ t₂ l r ih_l ih_r =>
     right
-    cases ih_l l with
+    cases ih_l rfl l with
     | inl val_l =>
-        cases ih_r r with
+        cases ih_r rfl r with
         | inl val_r =>
             have ⟨σ, t₁, eq⟩ := l.canonical_form_abs val_l
             exists t₁ ^ᵗᵗ t₂
@@ -97,7 +97,7 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t'
         grind
   case tapp σ' der _ ih =>
     right
-    specialize ih der
+    specialize ih rfl der
     cases ih with
     | inl val =>
         obtain ⟨_, t, _⟩ := der.canonical_form_tabs val
@@ -107,9 +107,9 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t'
         obtain ⟨t', _⟩ := red
         exists .tapp t' σ'
         grind
-  case let' t₁ σ t₂ τ L der _ _ ih =>
+  case let' t₁ σ t₂ τ L der _ ih _ =>
     right
-    cases ih der with
+    cases ih rfl der with
     | inl _ =>
         exists t₂ ^ᵗᵗ t₁
         grind
@@ -118,24 +118,24 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t'
         exists t₁'.let' t₂
         grind
   case inl der _ ih =>
-    cases (ih der) with
+    cases (ih rfl der) with
     | inl val => grind
     | inr red =>
         right
         obtain ⟨t', _⟩ := red
         exists .inl t'
         grind
   case inr der _ ih =>
-    cases (ih der) with
+    cases (ih rfl der) with
     | inl val => grind
     | inr red =>
         right
         obtain ⟨t', _⟩ := red
         exists .inr t'
         grind
-  case case t₁ _ _ t₂ _ t₃ _ der _ _ _ _ ih =>
+  case case t₁ _ _ t₂ _ t₃ _ der _ _ ih _ _ =>
     right
-    cases ih der with
+    cases ih rfl der with
     | inl val =>
         have ⟨t₁, lr⟩ := der.canonical_form_sum val
         cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind

Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean

@@ -264,7 +264,7 @@ lemma biorth_least_fact (G : Set P) :
       symm at hF ⊢
       apply ClosureOperator.IsClosed.closure_eq (congrArg orthogonal (congrArg orthogonal hF))
     have hF_closed : c.IsClosed F := (c.isClosed_iff).2 this.symm
-    simpa [c] using ClosureOperator.closure_min hGF hF_closed
+    simpa [c] using! ClosureOperator.closure_min hGF hF_closed
   apply h_min
 
 /-- `0` is the least fact (w.r.t. inclusion). -/
@@ -304,7 +304,7 @@ lemma inter_isFact_of_isFact {A B : Set P}
   let FB : Fact P := ⟨B, hB⟩
   have h := sInf_isFact (S := ({FA, FB} : Set (Fact P)))
   simpa [carriersInf, Set.image_pair, sInf_insert, sInf_singleton, inf_eq_inter]
-    using h
+    using! h
 
 instance : InfSet (Fact P) where
   sInf S := ⟨carriersInf S, sInf_isFact (S := S)⟩