chore: fixes for leanprover/lean4#2790

Archive/Imo/Imo1960Q1.lean

@@ -95,7 +95,12 @@ theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n :
   have := searchUpTo_start
   iterate 82
     replace :=
-      searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num)
+      searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl)
+        (by -- This used to be just `norm_num`, but after leanprover/lean4#2790,
+            -- that triggers a max recursion depth exception. As a workaround, we
+            -- manually rewrite with `Nat.digits_of_two_le_of_pos` first.
+            rw [Nat.digits_of_two_le_of_pos (by norm_num) (by norm_num)]
+            norm_num)
   exact searchUpTo_end this
 #align imo1960_q1.right_direction Imo1960Q1.right_direction
 

Archive/Imo/Imo1962Q1.lean

@@ -131,7 +131,17 @@ Now we combine these cases to show that 153846 is the smallest solution.
 
 
 theorem satisfied_by_153846 : ProblemPredicate 153846 := by
-  norm_num [ProblemPredicate]
+  -- This proof used to be the single line `norm_num [ProblemPredicate]`.
+  -- After leanprover/lean4#2790, that triggers a max recursion depth exception.
+  -- As a workaround, we manually apply `Nat.digits_of_two_le_of_pos` a few times
+  -- before invoking `norm_num`.
+  unfold ProblemPredicate
+  have two_le_ten : 2 ≤ 10 := by norm_num
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  norm_num
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
 
 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -29,7 +29,13 @@ local notation "‖" x "‖" => Fintype.card x
 /-- **Birthday Problem**: set cardinality interpretation. -/
 theorem birthday :
     2 * ‖Fin 23 ↪ Fin 365‖ < ‖Fin 23 → Fin 365‖ ∧ 2 * ‖Fin 22 ↪ Fin 365‖ > ‖Fin 22 → Fin 365‖ := by
-  simp only [Nat.descFactorial, Fintype.card_fin, Fintype.card_embedding_eq, Fintype.card_fun]
+  -- This used to be
+  -- `simp only [Nat.descFactorial, Fintype.card_fin, Fintype.card_embedding_eq, Fintype.card_fun]`
+  -- but after leanprover/lean4#2790 that triggers a max recursion depth exception.
+  -- As a workaround, we make some of the reduction steps more explicit.
+  rw [Fintype.card_embedding_eq, Fintype.card_fun, Fintype.card_fin, Fintype.card_fin]
+  rw [Fintype.card_embedding_eq, Fintype.card_fun, Fintype.card_fin, Fintype.card_fin]
+  simp only
 #align theorems_100.birthday Theorems100.birthday
 
 section MeasureTheory
@@ -72,9 +78,12 @@ theorem birthday_measure :
   generalize_proofs hfin
   have : |hfin.toFinset| = 42200819302092359872395663074908957253749760700776448000000 := by
     trans ‖Fin 23 ↪ Fin 365‖
-    · simp_rw [← Fintype.card_coe, Set.Finite.coeSort_toFinset, Set.coe_setOf]
-      exact Fintype.card_congr (Equiv.subtypeInjectiveEquivEmbedding _ _)
-    · simp only [Fintype.card_embedding_eq, Fintype.card_fin, Nat.descFactorial]
+    · rw [← Fintype.card_coe]
+      apply Fintype.card_congr
+      rw [Set.Finite.coeSort_toFinset, Set.coe_setOf]
+      exact Equiv.subtypeInjectiveEquivEmbedding _ _
+    · rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin]
+      rfl
   rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff]
   rotate_left; (iterate 2 right; norm_num); (iterate 2 left; norm_num)
   norm_cast

Mathlib/FieldTheory/RatFunc.lean

@@ -703,7 +703,7 @@ def liftMonoidWithZeroHom (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀⁰.co
   map_one' := by
     dsimp only -- porting note: force the function to be applied
     rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk]
-    simp only [map_one, Submonoid.coe_one, div_one]
+    simp only [map_one, OneMemClass.coe_one, div_one]
   map_mul' x y := by
     cases' x with x
     cases' y with y

Mathlib/Topology/Basic.lean

@@ -848,7 +848,7 @@ scoped[Topology] notation "𝓝" => nhds
 scoped[Topology] notation "𝓝[" s "] " x:100 => nhdsWithin x s
 
 /-- Notation for the filter of punctured neighborhoods of a point. -/
-scoped[Topology] notation "𝓝[≠] " x:100 => nhdsWithin x {x}ᶜ
+scoped[Topology] notation "𝓝[≠] " x:100 => nhdsWithin x (@singleton _ (Set _) instSingletonSet x)ᶜ
 
 /-- Notation for the filter of right neighborhoods of a point. -/
 scoped[Topology] notation "𝓝[≥] " x:100 => nhdsWithin x (Set.Ici x)

Mathlib/Util/DischargerAsTactic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 Alex J. Best. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
+import Lean.Meta.Tactic.Simp.Main
+import Lean.Elab.Tactic.Basic
 import Std.Tactic.Exact
 
 /-!

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
+    "rev": "7fcae402e28f1e06fb53eda892a3fdf26aea1c1c",
     "opts": {},
     "name": "std",
-    "inputRev?": "main",
+    "inputRev?": "nightly-testing",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
@@ -17,13 +17,21 @@
     "name": "Qq",
     "inputRev?": "master",
     "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "a76881668efab6e48a4f3333ad7ba894e8095b04",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "nightly-testing",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
     "opts": {},
     "name": "Cli",
-    "inputRev?": "main",
+    "inputRev?": "nightly",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -32,13 +40,5 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.21",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
     "inherited": false}}],
  "name": "mathlib"}

lakefile.lean

@@ -46,10 +46,10 @@ lean_exe checkYaml where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/leanprover/std4" @ "nightly-testing"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
-require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
-require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
+require aesop from git "https://github.com/leanprover-community/aesop" @ "nightly-testing"
+require Cli from git "https://github.com/leanprover/lean4-cli" @ "nightly"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.21"
 
 lean_lib Cache where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4-pr-releases:pr-release-2790