move(data/prod/*): A prod folder (#13771)

Create folder `data.prod.` to hold `prod` files and related types. Precisely:
* `data.prod` → `data.prod.basic`
* `data.pprod` → `data.prod.pprod`
* `data.tprod` → `data.prod.tprod`
* `order.lexicographic` → `data.prod.lex`

src/algebra/order/rearrangement.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys
 -/
 import algebra.order.module
+import data.prod.lex
 import group_theory.perm.support
-import order.lexicographic
 import order.monovary
 import tactic.abel
 

src/combinatorics/colex.lean

@@ -37,7 +37,7 @@ Related files are:
 * `data.list.lex`: Lexicographic order on lists.
 * `data.psigma.order`: Lexicographic order on `Σ' i, α i`.
 * `data.sigma.order`: Lexicographic order on `Σ i, α i`.
-* `order.lexicographic`: Lexicographic order on `α × β`.
+* `data.prod.lex`: Lexicographic order on `α × β`.
 
 ## Tags
 colex, colexicographic, binary

src/data/fin/tuple/sort.lean

@@ -6,7 +6,7 @@ Authors: Kyle Miller
 
 import data.fin.basic
 import data.finset.sort
-import order.lexicographic
+import data.prod.lex
 
 /-!
 

src/data/list/lex.lean

@@ -19,7 +19,7 @@ Related files are:
 * `data.finset.colex`: Colexicographic order on finite sets.
 * `data.psigma.order`: Lexicographic order on `Σ' i, α i`.
 * `data.sigma.order`: Lexicographic order on `Σ i, α i`.
-* `order.lexicographic`: Lexicographic order on `α × β`.
+* `data.prod.lex`: Lexicographic order on `α × β`.
 -/
 
 namespace list

src/data/pi/algebra.lean

@@ -3,12 +3,13 @@ Copyright (c) 2020 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
-import tactic.split_ifs
-import tactic.simpa
-import tactic.congr
 import algebra.group.to_additive
-import data.prod
+import data.prod.basic
 import logic.unique
+import tactic.congr
+import tactic.simpa
+import tactic.split_ifs
+
 /-!
 # Instances and theorems on pi types
 

src/order/lexicographic.lean → src/data/prod/lex.lean

@@ -8,12 +8,10 @@ import order.synonym
 /-!
 # Lexicographic order
 
-This file defines the lexicographic relation for pairs and dependent pairs of orders, partial orders
-and linear orders.
+This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.
 
 ## Main declarations
 
-* `lex α`: A type synonym of `α` to equip it with its lexicographic order.
 * `prod.lex.<pre/partial_/linear_>order`: Instances lifting the orders on `α` and `β` to `α ×ₗ β`.
 
 ## Notation

src/data/psigma/order.lean

@@ -23,7 +23,7 @@ Related files are:
 * `data.finset.colex`: Colexicographic order on finite sets.
 * `data.list.lex`: Lexicographic order on lists.
 * `data.sigma.order`: Lexicographic order on `Σₗ i, α i`. Basically a twin of this file.
-* `order.lexicographic`: Lexicographic order on `α × β`.
+* `data.prod.lex`: Lexicographic order on `α × β`.
 
 ## TODO
 

src/data/sigma/lex.lean

@@ -23,7 +23,7 @@ Related files are:
 * `data.list.lex`: Lexicographic order on lists.
 * `data.sigma.order`: Lexicographic order on `Σ i, α i` per say.
 * `data.psigma.order`: Lexicographic order on `Σ' i, α i`.
-* `order.lexicographic`: Lexicographic order on `α × β`. Can be thought of as the special case of
+* `data.prod.lex`: Lexicographic order on `α × β`. Can be thought of as the special case of
   `sigma.lex` where all summands are the same
 -/
 

src/data/sigma/order.lean

@@ -28,7 +28,7 @@ Related files are:
 * `data.finset.colex`: Colexicographic order on finite sets.
 * `data.list.lex`: Lexicographic order on lists.
 * `data.psigma.order`: Lexicographic order on `Σₗ' i, α i`. Basically a twin of this file.
-* `order.lexicographic`: Lexicographic order on `α × β`.
+* `data.prod.lex`: Lexicographic order on `α × β`.
 
 ## TODO
 

src/logic/embedding.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import data.fun_like.embedding
-import data.pprod
+import data.prod.pprod
 import data.set.basic
 import data.sigma.basic
 import logic.equiv.basic

src/logic/equiv/basic.lean

@@ -5,11 +5,11 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import data.fun_like.equiv
 import data.option.basic
-import data.prod
+import data.prod.basic
 import data.quot
 import data.sigma.basic
-import data.sum.basic
 import data.subtype
+import data.sum.basic
 import logic.function.conjugate
 import logic.unique
 import tactic.norm_cast

src/logic/nontrivial.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import data.prod
+import data.prod.basic
 import data.subtype
 import logic.function.basic
 import logic.unique

src/measure_theory/measurable_space.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 
 import algebra.indicator_function
-import data.tprod
+import data.prod.tprod
 import group_theory.coset
 import logic.equiv.fin
 import measure_theory.measurable_space_def

src/order/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro
 -/
-import data.prod
+import data.prod.basic
 import data.subtype
 
 /-!
@@ -564,7 +564,7 @@ end subtype
 /-!
 ### Pointwise order on `α × β`
 
-The lexicographic order is defined in `order.lexicographic`, and the instances are available via the
+The lexicographic order is defined in `data.prod.lex`, and the instances are available via the
 type synonym `α ×ₗ β = α × β`.
 -/
 

src/order/filter/bases.lean

@@ -3,9 +3,9 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
-import order.filter.basic
+import data.prod.pprod
 import data.set.countable
-import data.pprod
+import order.filter.basic
 
 /-!
 # Filter bases

src/tactic/core.lean

@@ -16,7 +16,7 @@ universe u
 
 attribute [derive [has_reflect, decidable_eq]] tactic.transparency
 
--- Rather than import order.lexicographic here, we can get away with defining the order by hand.
+-- Rather than import data.prod.lex here, we can get away with defining the order by hand.
 instance : has_lt pos :=
 { lt := λ x y, x.line < y.line ∨ x.line = y.line ∧ x.column < y.column }
 

src/tactic/linarith/preprocessing.lean

@@ -3,11 +3,10 @@ Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
-
+import data.prod.lex
+import tactic.cancel_denoms
 import tactic.linarith.datatypes
 import tactic.zify
-import tactic.cancel_denoms
-import order.lexicographic
 
 /-!
 # Linarith preprocessing