chore(deps): advance CSLib and Mathlib on Lean rc2

Complexity/Algorithms/Reachability/InductiveCounting/Completeness.lean

@@ -357,7 +357,7 @@ theorem accepts_complete (hsource : source < N) (hwidth : N ≤ 2 ^ width)
     exact h _ _ rfl (invariant_initial hsource) bounded_initial (honest_initial hsource)
   intro n
   induction n using Nat.strong_induction_on with
-  | h n ih =>
+  | ind n ih =>
     intro s hr hi hb hh
     by_cases hs : halted s = true
     · refine ⟨[], ?_⟩
@@ -400,7 +400,7 @@ theorem exists_replay_done_final (hsource : source < N) (hwidth : N ≤ 2 ^ widt
       (by simp [initial, hsource])
   intro n
   induction n using Nat.strong_induction_on with
-  | h n ih =>
+  | ind n ih =>
     intro s hr hi hb hh hna
     by_cases hdone : s.phase = .done ∧ s.finalScan = true
     · refine ⟨[], hdone.1, hdone.2, ?_⟩

Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean

@@ -519,7 +519,7 @@ private theorem one_le_priority (i : Fin g) : 1 ≤ P.priority i := by
   suffices ∀ k : ℕ, ∀ i : Fin g, g - 1 - i.val = k → 1 ≤ P.priority i from this _ i rfl
   intro k
   induction k using Nat.strong_induction_on with
-  | h k ih =>
+  | ind k ih =>
     intro i hik
     rw [P.priority_eq]
     suffices 0 ≤ ∑ j : Fin g, if i < j then P.priority j * |P.gateWeight j i| else 0 by linarith
@@ -566,7 +566,7 @@ theorem priority_le_pow {W : ℝ} (hW0 : 0 ≤ W)
   suffices ∀ m : ℕ, ∀ i : Fin g, g - 1 - i.val = m → P.priority i ≤ (W + 1) ^ m from this _ i rfl
   intro m
   induction m using Nat.strong_induction_on with
-  | h m ih =>
+  | ind m ih =>
     intro i him
     rw [P.priority_eq, ← one_add_mul_sum_geom W m]
     have hsum : (∑ j : Fin g, if i < j then P.priority j * |P.gateWeight j i| else 0) ≤

Complexity/Computability/Circuit/Frontier/BranchingProgram.lean

@@ -378,7 +378,7 @@ theorem abs_signedCount_accepted_le [Finite ι] [Finite U] [Finite M] (hP : P.Un
     (hS : RectangleBias S K b) :
     |signedCount S P.accepted| ≤ 2 * b * P.accepted.ncard + ((K - 1) ^ 2 * P.size : ℕ) := by
   induction hn : P.accepted.ncard using Nat.strong_induction_on generalizing P with
-  | h n ih =>
+  | ind n ih =>
     subst hn
     by_cases hthick : ∃ t ≤ P.length, ∃ x ∈ P.accepted,
         K ≤ (P.sweep.pastSide t x).ncard ∧ K ≤ (P.sweep.futureSide t x).ncard

Complexity/Computability/Circuit/Rational/LaurentReduction.lean

@@ -262,7 +262,7 @@ theorem exists_integralFrame {ι : Type*} [Finite ι]
     this _ U rfl
   intro k
   induction k using Nat.strong_induction_on with
-  | h k ih =>
+  | ind k ih =>
     intro U hdim
     by_cases hU : U = ⊥
     · subst U

Complexity/Computability/Circuit/Rational/Wronskian.lean

@@ -513,7 +513,7 @@ lemma low_coefficients_force_zero {K : Type*} [Field K] {h : ℕ}
   have hi : ∀ m, ∀ j, (f j).natTrailingDegree = m → m < r → c j = 0 := by
     intro m
     induction m using Nat.strong_induction_on with
-    | h m ih =>
+    | ind m ih =>
       intro j hj hmr
       have hs : (∑ k, c k • f k).coeff m = c j * (f j).coeff m := by
         simp only [finsetSum_coeff, coeff_smul, smul_eq_mul]

Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Bounds.lean

@@ -88,7 +88,7 @@ theorem choose_inWindow {input : List Bool} (Inv : (Fin k → List Bool) → Pro
       ∀ ws out, Inv ws → p.head = wordsCfg input (some .choose) ws out → p.InWindow s := by
     intro n
     induction n using Nat.strong_induction_on with
-    | h n ih =>
+    | ind n ih =>
       intro p hlen ws out hInv hhead
       by_cases hzero : p.length = 0
       · rintro _ ⟨j, rfl⟩ i

Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean

@@ -153,7 +153,7 @@ theorem choose_output (a : α) (p : R.machine.RunPath (enc a)) (s : σ)
         p.last.output = out ++ [M.accept s'] := by
     intro n
     induction n using Nat.strong_induction_on with
-    | h n ih =>
+    | ind n ih =>
       intro p hn s hs flag out hhead hhalt
       have hpos : 0 < p.length := by
         by_contra hz

Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Termination.lean

@@ -75,7 +75,7 @@ theorem choose_haltsFrom {input : List Bool} (Inv : (Fin k → List Bool) → Pr
       ∃ t, HaltsFrom I P F C (wordsCfg input (some .choose) ws out) t := by
     intro n
     induction n using Nat.strong_induction_on with
-    | h n ih =>
+    | ind n ih =>
       intro ws hr hInv out
       have branches : ∀ b, ∃ t, HaltsFrom I P F C
           (wordsCfg input (some (.pass b (P b).q₀)) ws out) t := by

Complexity/Computability/WordRAM/GhostLoop.lean

@@ -44,7 +44,7 @@ theorem ExecWithin.loop_invariant_state {B : Basis} {r w T : ℕ} {σ : Type*}
         I s' y ∧ ¬cond.Holds y := by
     intro n
     induction n using Nat.strong_induction_on with
-    | h n ih =>
+    | ind n ih =>
       intro s x hμ hI
       by_cases hc : cond.Holds x
       · obtain ⟨s₁, y, hy, hIy, hdec⟩ := hbody s x hI hc

Complexity/Foundations/Combinatorics/FunctionalGraph/ForestSegments.lean

@@ -174,7 +174,7 @@ theorem forest_hull_partition {L : ℕ} (hL : 0 < L)
       f^[t] a ∈ forestMarks f H ∨ ∃ b d i, IsForestEdge f H b d ∧
         d ≤ 2 * L ∧ i < d ∧ f^[i] b = f^[t] a := by
     induction t using Nat.strong_induction_on with
-    | h t ih =>
+    | ind t ih =>
       intro a ha ht
       by_cases hz : t = 0
       · subst t

Complexity/Foundations/NumberTheory/Harmonic.lean

@@ -78,7 +78,7 @@ theorem two_mul_sum_add_one_mul_harmonic (m : ℕ) :
 theorem harmonic_le_log_add_one (n : ℕ) :
     harmonic n ≤ (Nat.log 2 n : ℚ) + 1 := by
   induction n using Nat.strong_induction_on with
-  | h n ih =>
+  | ind n ih =>
     rcases lt_or_ge n 2 with hn2 | hn2
     · interval_cases n <;> norm_num [harmonic]
     · set half := n / 2

Complexity/Foundations/NumberTheory/PrimeCounting.lean

@@ -143,7 +143,7 @@ theorem lcmUpto_add_le {m n : ℕ} (h : n ≤ m) :
 theorem two_mul_lcmUpto_le_four_pow (n : ℕ) (hn : 1 ≤ n) :
     2 * Nat.lcmUpto n ≤ 4 ^ n := by
   induction n using Nat.strong_induction_on with
-  | h n ihn =>
+  | ind n ihn =>
     rcases le_or_gt n 2 with hn2 | hn2
     · interval_cases n <;> decide
     · rcases n.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩

docbuild/lake-manifest.json

@@ -73,20 +73,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad",
+   "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a",
    "name": "cslib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad",
+   "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d581dfff2e41de989072ea63abf3daf69311520",
+   "rev": "69552756cd8a2d2d48763cf7279fd814d6a1224d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc2",
+   "inputRev": "69552756cd8a2d2d48763cf7279fd814d6a1224d",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",

guide/lake-manifest.json

@@ -73,20 +73,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad",
+   "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a",
    "name": "cslib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad",
+   "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d581dfff2e41de989072ea63abf3daf69311520",
+   "rev": "69552756cd8a2d2d48763cf7279fd814d6a1224d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc2",
+   "inputRev": "69552756cd8a2d2d48763cf7279fd814d6a1224d",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad",
+   "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a",
    "name": "cslib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad",
+   "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d581dfff2e41de989072ea63abf3daf69311520",
+   "rev": "69552756cd8a2d2d48763cf7279fd814d6a1224d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc2",
+   "inputRev": "69552756cd8a2d2d48763cf7279fd814d6a1224d",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",

lakefile.toml

@@ -33,7 +33,7 @@ autoImplicit = false
 [[require]]
 name = "cslib"
 git = "https://github.com/leanprover/cslib"
-rev = "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad"
+rev = "254e30e6d4299c51323aaeaf5f51a4763b375d4a"
 
 [[lean_lib]]
 name = "Complexity"