From 449de2e42af49b1cb0411f8d8905dd26c2f93e5f Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 31 Oct 2024 07:37:54 +0100
Subject: [PATCH] Update mathlib

---
 Nevanlinna/specialFunctions_Integral_log_sin.lean | 2 +-
 lake-manifest.json                                | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Nevanlinna/specialFunctions_Integral_log_sin.lean b/Nevanlinna/specialFunctions_Integral_log_sin.lean
index e70488b..1a968e6 100644
--- a/Nevanlinna/specialFunctions_Integral_log_sin.lean
+++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean
@@ -24,7 +24,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
     exact zero_lt_two
     apply (Set.mem_Icc.1 hx).1
     simp
-    apply mul_le_one
+    apply mul_le_one₀
     rw [div_le_one pi_pos]
     exact two_le_pi
     exact (Set.mem_Icc.1 hx).1
diff --git a/lake-manifest.json b/lake-manifest.json
index 07bd132..ab410a8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6",
+   "rev": "500a529408399c44d7e1649577e3c98697f95aa4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0ea83a676d288220ba227808568cbb80fe43ace0",
+   "rev": "c1970bea80ac3357a6a991a6d00d12e7435c12c7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "893b3a846645d48ac45143ec02149cc551acd99d",
+   "rev": "d9273054fe5aee13954cca827d9bbfe7a01bde67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,