Bump to v4.21.0 (#424)

Author: Ruben-VandeVelde

Carleson/Psi.lean

@@ -554,7 +554,7 @@ lemma norm_Ks_le {s : ℤ} {x y : X} :
   · apply le_trans <| norm_K_le 0 (mem_Icc.1 (dist_mem_Icc_of_Ks_ne_zero hK)).1
     rw [pow_zero, one_mul, Nat.cast_zero, add_zero]
     suffices 2 * (a : ℝ) + 101 * a ^ 3 ≤ 102 * a ^ 3 by
-      gcongr; simpa [C2_1_3, ← Real.rpow_natCast] using this
+      gcongr; simpa [C2_1_3, ← Real.rpow_natCast, -Real.rpow_ofNat] using this
     suffices 2 * (a : ℝ) ≤ a ^ 2 * a by linarith
     nlinarith [show 4 ≤ (a : ℝ) by exact_mod_cast four_le_a X]
   · exact abs_ψ_le_one D (D ^ (-s) * dist x y)
@@ -803,8 +803,8 @@ private lemma norm_Ks_sub_Ks_le₁ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0)
       refine le_of_eq_of_le ?_ <|
         (Real.strictAnti_rpow_of_base_lt_one (by norm_num) (by norm_num)).antitone a_inv_le
       rw [← Real.rpow_left_inj (by positivity) (by positivity) three_pos.ne.symm]
+      rw [← Real.rpow_mul (by norm_num)]
       norm_num
-      simp
   have hlt : 0 < (D2_1_3 a : ℝ) := by simp [D2_1_3]
   have : D2_1_3 a * (dist y y' / D ^ s) ^ (a : ℝ)⁻¹ ≥
       D2_1_3 a * (2 : ℝ) ^ (-100 * a + (-1 : ℝ)) := mod_cast ((mul_lt_mul_left hlt).2 key).le

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "87e776fcdaac566a75f44d485042443d57959bcb",
+   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1603151ac0db4e822908e18094f16acc250acaff",
+   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e25fe66cf13e902ba550533ef681cc35a9f18dc2",
+   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1b1abe64060b3e3250218646023e47950d8cd396",
+   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d6afe6744246a799a3564dc84a878dab0c4a56d8",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d12fdadd81cb96980327cc02587fc14dea65a6e0",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "a0abd472348dd725adbb26732e79b26e7e220913",
+   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.21.0-rc3
+leanprover/lean4:v4.21.0