chore: bump to mathlib 4.20 (#371)

Author: grunweg

Carleson/ToMathlib/Analysis/Normed/Group/Basic.lean

@@ -18,23 +18,4 @@ theorem enorm_multiset_prod_le [ENormedCommMonoid E] (m : Multiset E) :
   · simp [enorm_one', ofAdd_zero]
   · exact enorm_mul_le' x y
 
-@[bound]
-theorem enorm_sum_le [ENormedAddCommMonoid E] (s : Finset ι) (f : ι → E) :
-    ‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ :=
-  s.le_sum_of_subadditive enorm enorm_zero enorm_add_le f
-
-@[to_additive existing]
-theorem enorm_prod_le [ENormedCommMonoid E] (s : Finset ι) (f : ι → E) :
-    ‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ := by
-  rw [← Multiplicative.ofAdd_le, ofAdd_sum]
-  refine Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ enorm) ?_ (fun x y => ?_) _ _
-  · simp [enorm_one', ofAdd_zero]
-  · exact enorm_mul_le' x y
-
-@[to_additive]
-theorem enorm_prod_le_of_le [ENormedCommMonoid E] (s : Finset ι) {f : ι → E} {n : ι → ℝ≥0∞}
-      (h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b) :
-    ‖∏ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b :=
-  (enorm_prod_le s f).trans <| Finset.sum_le_sum h
-
 end ENormedMonoid

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cccd832d981238b7092510beead89f13e7d1ac87",
+   "rev": "c8e33dbbce6b29c9635f1768486535b74eb67402",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "304c5e2f490d546134c06bf8919e13b175272084",
+   "rev": "2ac43674e92a695e96caac19f4002b25434636da",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48",
+   "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a",
+   "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.59",
+   "inputRev": "v0.0.60",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a1cfb751fd148b5dedfc3ebe2f638d71d7ecad0c",
+   "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130",
+   "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "233a67fdba5cb0ff0e2136d7eded5fb29916dc2b",
+   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
+   "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.0-rc5
+leanprover/lean4:v4.20.0