From 04ba6a9ee68c398149270bceddaf8e3519017114 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 31 Jul 2024 07:43:20 +0000
Subject: [PATCH] Bump mathlib

---
 LeanAPAP.lean                                     |  1 -
 LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean   | 15 ---------------
 .../MeasureTheory/Function/LpSeminorm/Basic.lean  |  6 +++---
 LeanAPAP/Prereqs/Expect/Basic.lean                |  1 -
 LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean        |  1 -
 lake-manifest.json                                |  2 +-
 6 files changed, 4 insertions(+), 22 deletions(-)
 delete mode 100644 LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean

diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index eaa083148f..db550b977d 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -5,7 +5,6 @@ import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 import LeanAPAP.Mathlib.Data.Rat.Cast.Defs
 import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
diff --git a/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean b/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean
deleted file mode 100644
index 942ac5d1ce..0000000000
--- a/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import Mathlib.Data.Fintype.BigOperators
-
-open Finset
-
-namespace Fintype
-variable {α β : Type*} {δ : α → Type*} {s : Finset α} {n : ℕ}
-
-local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
-
-protected lemma _root_.Finset.Nonempty.piFinset_const (hs : s.Nonempty) : (s ^^ n).Nonempty :=
-  piFinset_nonempty.2 fun _ ↦ hs
-
-lemma card_piFinset_const (s : Finset α) (n : ℕ) : (s ^^ n).card = s.card ^ n := by simp
-
-end Fintype
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index 02e3edac35..f0ca4d4b8d 100644
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -6,8 +6,8 @@ open scoped NNReal ENNReal Topology
 
 variable {α E : Type*} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E]
 
-lemma snormEssSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → E) : snormEssSup f μ = ⨆ a, ↑‖f a‖₊ :=
+lemma eLpNormEssSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → E) : eLpNormEssSup f μ = ⨆ a, ↑‖f a‖₊ :=
   essSup_eq_iSup hμ _
 
-@[simp] lemma snormEssSup_count [MeasurableSingletonClass α] (f : α → E) :
-    snormEssSup f .count = ⨆ a, ↑‖f a‖₊ := essSup_count _
+@[simp] lemma eLpNormEssSup_count [MeasurableSingletonClass α] (f : α → E) :
+    eLpNormEssSup f .count = ⨆ a, ↑‖f a‖₊ := essSup_count _
diff --git a/LeanAPAP/Prereqs/Expect/Basic.lean b/LeanAPAP/Prereqs/Expect/Basic.lean
index ef6526734d..0ab3ea0c5a 100644
--- a/LeanAPAP/Prereqs/Expect/Basic.lean
+++ b/LeanAPAP/Prereqs/Expect/Basic.lean
@@ -3,7 +3,6 @@ import Mathlib.Algebra.Order.Module.Rat
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Algebra.Algebra.Basic
-import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 
 /-!
 # Average over a finset
diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
index 789ab2f518..83b0d5628a 100644
--- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
+++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -1,5 +1,4 @@
 import Mathlib.Analysis.MeanInequalitiesPow
-import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 import LeanAPAP.Prereqs.Multinomial
 
 open Finset Fintype Nat Real
diff --git a/lake-manifest.json b/lake-manifest.json
index d1d1b40fc3..fca0319862 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "db8dc843e42d4ce957d1919227451a23c24d7b95",
+   "rev": "09e1ab33b2621aba98326aee36572a878b092875",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,