From 5f3f7173f52699141d35032efcd7b06348b1e8be Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 1 Jan 2025 20:40:43 +0100 Subject: [PATCH] Update mathlib --- Nevanlinna/meromorphicAt.lean | 2 +- lake-manifest.json | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean index d1c3e19..fdd9fab 100644 --- a/Nevanlinna/meromorphicAt.lean +++ b/Nevanlinna/meromorphicAt.lean @@ -223,7 +223,7 @@ theorem AnalyticAt.meromorphicAt_order_nonneg 0 ≤ hf.meromorphicAt.order := by rw [hf.meromorphicAt_order] rw [(by rfl : (0 : WithTop ℤ) = WithTop.map Nat.cast (0 : ℕ∞))] - rw [WithTop.map_le_iff] + erw [WithTop.map_le_iff] simp; simp diff --git a/lake-manifest.json b/lake-manifest.json index 700c077..0720952 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "054d75b44095e8390c2afd9744e30c3b2b6cbd42", + "rev": "504007f6f772de93ea967b17320baeac5a21cb55", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4", + "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9e583efcea920afa13ee2a53069821a2297a94c0", + "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",