From 586e58a4ba5bbe287bc329a4c29569e8d613ad82 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 13 Nov 2024 22:09:06 +0000
Subject: [PATCH] chore: move pointwise set files to `Algebra._.Pointwise`

---
 Mathlib.lean                                  |  9 +++---
 Mathlib/Algebra/Algebra/Operations.lean       |  2 +-
 .../Algebra/Group/Pointwise/Finset/Basic.lean |  4 +--
 .../Group/Pointwise/Finset/Interval.lean      |  2 +-
 .../Group/Pointwise/Set}/BigOperators.lean    |  0
 Mathlib/Algebra/Group/Pointwise/Set/Card.lean |  2 +-
 .../Group/Pointwise/Set}/Finite.lean          |  0
 .../Group/Pointwise/Set}/ListOfFn.lean        |  0
 .../Algebra/Order/Group/Pointwise/Bounds.lean |  2 ++
 .../Order/Group}/Pointwise/Interval.lean      |  0
 Mathlib/Analysis/Normed/Field/Basic.lean      |  4 +--
 Mathlib/Data/Real/Cardinality.lean            |  2 +-
 Mathlib/Data/Set/Pointwise/BoundedMul.lean    | 28 -------------------
 Mathlib/GroupTheory/Finiteness.lean           |  2 +-
 .../LinearAlgebra/AffineSpace/AffineMap.lean  |  2 +-
 Mathlib/Topology/Algebra/Order/Field.lean     |  2 +-
 Mathlib/Topology/MetricSpace/Pseudo/Real.lean |  2 +-
 17 files changed, 18 insertions(+), 45 deletions(-)
 rename Mathlib/{Data/Set/Pointwise => Algebra/Group/Pointwise/Set}/BigOperators.lean (100%)
 rename Mathlib/{Data/Set/Pointwise => Algebra/Group/Pointwise/Set}/Finite.lean (100%)
 rename Mathlib/{Data/Set/Pointwise => Algebra/Group/Pointwise/Set}/ListOfFn.lean (100%)
 rename Mathlib/{Data/Set => Algebra/Order/Group}/Pointwise/Interval.lean (100%)
 delete mode 100644 Mathlib/Data/Set/Pointwise/BoundedMul.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index ef683fa1d3328d..2e2943f877c418 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -289,7 +289,10 @@ import Mathlib.Algebra.Group.Pi.Lemmas
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Algebra.Group.Pointwise.Finset.Interval
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
+import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import Mathlib.Algebra.Group.Pointwise.Set.Card
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
+import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Semiconj.Basic
 import Mathlib.Algebra.Group.Semiconj.Defs
@@ -648,6 +651,7 @@ import Mathlib.Algebra.Order.Group.OrderIso
 import Mathlib.Algebra.Order.Group.PiLex
 import Mathlib.Algebra.Order.Group.Pointwise.Bounds
 import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Group.Synonym
@@ -2797,12 +2801,7 @@ import Mathlib.Data.Set.Operations
 import Mathlib.Data.Set.Opposite
 import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Data.Set.Pairwise.Lattice
-import Mathlib.Data.Set.Pointwise.BigOperators
-import Mathlib.Data.Set.Pointwise.BoundedMul
-import Mathlib.Data.Set.Pointwise.Finite
-import Mathlib.Data.Set.Pointwise.Interval
 import Mathlib.Data.Set.Pointwise.Iterate
-import Mathlib.Data.Set.Pointwise.ListOfFn
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Data.Set.Pointwise.Support
 import Mathlib.Data.Set.Prod
diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
index 33686a95e9ef48..b39f7aaf5c8b1c 100644
--- a/Mathlib/Algebra/Algebra/Operations.lean
+++ b/Mathlib/Algebra/Algebra/Operations.lean
@@ -6,9 +6,9 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Algebra.Opposite
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.Module.Submodule.Pointwise
-import Mathlib.Data.Set.Pointwise.BigOperators
 import Mathlib.Data.Set.Semiring
 import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
 
diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
index a7cd803e05c074..7deb89fb1b3813 100644
--- a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
+++ b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@@ -5,11 +5,11 @@ Authors: Floris van Doorn, Yaël Dillies
 -/
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Group.Action.Pi
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
 import Mathlib.Data.Finset.Density
 import Mathlib.Data.Finset.Max
 import Mathlib.Data.Finset.NAry
-import Mathlib.Data.Set.Pointwise.Finite
-import Mathlib.Data.Set.Pointwise.ListOfFn
+import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
 import Mathlib.Data.Set.Pointwise.SMul
 
 /-!
diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
index 479121a3d4a1b9..d06c3e7259b133 100644
--- a/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
+++ b/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Order.Interval.Finset.Defs
 
 /-! # Pointwise operations on intervals
diff --git a/Mathlib/Data/Set/Pointwise/BigOperators.lean b/Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
similarity index 100%
rename from Mathlib/Data/Set/Pointwise/BigOperators.lean
rename to Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
index 80a073b792385c..bb228c7f134f5a 100644
--- a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
+++ b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Data.Set.Pointwise.Finite
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
 import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
diff --git a/Mathlib/Data/Set/Pointwise/Finite.lean b/Mathlib/Algebra/Group/Pointwise/Set/Finite.lean
similarity index 100%
rename from Mathlib/Data/Set/Pointwise/Finite.lean
rename to Mathlib/Algebra/Group/Pointwise/Set/Finite.lean
diff --git a/Mathlib/Data/Set/Pointwise/ListOfFn.lean b/Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean
similarity index 100%
rename from Mathlib/Data/Set/Pointwise/ListOfFn.lean
rename to Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean
diff --git a/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean
index d7e523a2a65957..ceb329876b8e6b 100644
--- a/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean
+++ b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean
@@ -48,6 +48,8 @@ lemma BddAbove.mul (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) :=
 lemma BddBelow.mul (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) :=
   (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)
 
+@[to_additive (attr := deprecated (since := "2024-11-13"))] alias Set.BddAbove.mul := BddAbove.mul
+
 @[to_additive]
 lemma BddAbove.range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) :
     BddAbove (range fun i ↦ f i * g i) :=
diff --git a/Mathlib/Data/Set/Pointwise/Interval.lean b/Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
similarity index 100%
rename from Mathlib/Data/Set/Pointwise/Interval.lean
rename to Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean
index a81ab41393a9d6..eb3c22b61051f6 100644
--- a/Mathlib/Analysis/Normed/Field/Basic.lean
+++ b/Mathlib/Analysis/Normed/Field/Basic.lean
@@ -5,10 +5,10 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 import Mathlib.Algebra.Algebra.NonUnitalSubalgebra
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Algebra.Field.Subfield.Defs
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.Analysis.Normed.Group.Submodule
-import Mathlib.Data.Set.Pointwise.Interval
-import Mathlib.Algebra.Field.Subfield.Defs
 
 /-!
 # Normed fields
diff --git a/Mathlib/Data/Real/Cardinality.lean b/Mathlib/Data/Real/Cardinality.lean
index 0ea501663c7c3d..f2c8ed9b0f521e 100644
--- a/Mathlib/Data/Real/Cardinality.lean
+++ b/Mathlib/Data/Real/Cardinality.lean
@@ -3,9 +3,9 @@ Copyright (c) 2019 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.Data.Rat.Denumerable
-import Mathlib.Data.Set.Pointwise.Interval
 import Mathlib.SetTheory.Cardinal.Continuum
 
 /-!
diff --git a/Mathlib/Data/Set/Pointwise/BoundedMul.lean b/Mathlib/Data/Set/Pointwise/BoundedMul.lean
deleted file mode 100644
index 2d630b685665ee..00000000000000
--- a/Mathlib/Data/Set/Pointwise/BoundedMul.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-/-
-Copyright (c) 2021 Yury Kudryashov. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury KudryashovJ
--/
-import Mathlib.Algebra.Group.Pointwise.Set.Basic
-import Mathlib.Algebra.Order.Monoid.Defs
-
-/-!
-
-# Pointwise multiplication of sets preserves boundedness above.
-
-TODO: Can be combined with future results about pointwise multiplication on sets that use
-ordered algebraic classes.
-
--/
-
-variable {α : Type*}
-
-namespace Set
-
-open Pointwise
-
-@[to_additive]
-theorem BddAbove.mul [OrderedCommMonoid α] {A B : Set α} (hA : BddAbove A) (hB : BddAbove B) :
-    BddAbove (A * B) :=
-  hA.image2 (fun _ _ _ h ↦ mul_le_mul_right' h _) (fun _ _ _ h ↦ mul_le_mul_left' h _) hB
-end Set
diff --git a/Mathlib/GroupTheory/Finiteness.lean b/Mathlib/GroupTheory/Finiteness.lean
index 80895c9fc92ee9..bd31d6b8743b43 100644
--- a/Mathlib/GroupTheory/Finiteness.lean
+++ b/Mathlib/GroupTheory/Finiteness.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
 import Mathlib.Algebra.Group.Subgroup.Pointwise
-import Mathlib.Data.Set.Pointwise.Finite
 import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.SetTheory.Cardinal.Finite
 
diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
index 71f99e5c85dde4..259da107ba0114 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.LinearAlgebra.AffineSpace.Basic
 import Mathlib.LinearAlgebra.BilinearMap
 import Mathlib.LinearAlgebra.Pi
diff --git a/Mathlib/Topology/Algebra/Order/Field.lean b/Mathlib/Topology/Algebra/Order/Field.lean
index 51f7585e7e00c8..ee7ea3caa64425 100644
--- a/Mathlib/Topology/Algebra/Order/Field.lean
+++ b/Mathlib/Topology/Algebra/Order/Field.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash
 -/
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Order.Filter.AtTopBot.Field
 import Mathlib.Topology.Algebra.Field
 import Mathlib.Topology.Algebra.Order.Group
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Real.lean b/Mathlib/Topology/MetricSpace/Pseudo/Real.lean
index ae477178577c56..baa4f534f75cca 100644
--- a/Mathlib/Topology/MetricSpace/Pseudo/Real.lean
+++ b/Mathlib/Topology/MetricSpace/Pseudo/Real.lean
@@ -3,7 +3,7 @@ Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
 -/
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Topology.MetricSpace.Pseudo.Pi
 
 /-!