chore: move Algebra/Group/ZeroOne/ to Data/ (#20622)

Minor cleanup on the path to reducing dependencies from Data/ on other top-level directories.

Author: kim-em

Mathlib.lean

@@ -373,7 +373,6 @@ import Mathlib.Algebra.Group.Units.Hom
 import Mathlib.Algebra.Group.Units.Opposite
 import Mathlib.Algebra.Group.WithOne.Basic
 import Mathlib.Algebra.Group.WithOne.Defs
-import Mathlib.Algebra.Group.ZeroOne
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.GroupWithZero.Action.Basic
 import Mathlib.Algebra.GroupWithZero.Action.Defs
@@ -979,6 +978,7 @@ import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.Algebra.Vertex.HVertexOperator
 import Mathlib.Algebra.Vertex.VertexOperator
+import Mathlib.Algebra.ZeroOne.Lemmas
 import Mathlib.AlgebraicGeometry.AffineScheme
 import Mathlib.AlgebraicGeometry.AffineSpace
 import Mathlib.AlgebraicGeometry.Cover.MorphismProperty
@@ -2846,6 +2846,7 @@ import Mathlib.Data.Num.Basic
 import Mathlib.Data.Num.Bitwise
 import Mathlib.Data.Num.Lemmas
 import Mathlib.Data.Num.Prime
+import Mathlib.Data.One.Defs
 import Mathlib.Data.Opposite
 import Mathlib.Data.Option.Basic
 import Mathlib.Data.Option.Defs

Mathlib/Algebra/Expr.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.Algebra.Group.ZeroOne
+import Mathlib.Data.One.Defs
 import Qq
 
 /-! # Helpers to invoke functions involving algebra at tactic time

Mathlib/Algebra/Group/Defs.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 import Mathlib.Data.Int.Notation
 import Mathlib.Data.Nat.BinaryRec
-import Mathlib.Algebra.Group.ZeroOne
+import Mathlib.Data.One.Defs
 import Mathlib.Algebra.Group.Operations
 import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.Simps.Basic

Mathlib/Algebra/NeZero.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
 import Mathlib.Logic.Basic
-import Mathlib.Algebra.Group.ZeroOne
+import Mathlib.Data.One.Defs
 import Mathlib.Order.Defs.PartialOrder
 
 /-!

Mathlib/Algebra/Order/Pi.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
+import Mathlib.Algebra.ZeroOne.Lemmas
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Ring.Pi

Mathlib/Algebra/Order/ZeroLEOne.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import Mathlib.Order.Basic
+import Mathlib.Data.One.Defs
 
 /-!
 # Typeclass expressing `0 ≤ 1`.

Mathlib/Algebra/ZeroOne/Lemmas.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2023 Yael Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yael Dillies
+-/
+import Batteries.Tactic.Init
+import Mathlib.Data.One.Defs
+import Mathlib.Tactic.ToAdditive
+import Mathlib.Tactic.Lemma
+
+/-! # Lemmas about inequalities with `1`. -/
+
+variable {α : Type _}
+
+section dite
+variable [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬ p → α}
+
+@[to_additive dite_nonneg]
+lemma one_le_dite [LE α] (ha : ∀ h, 1 ≤ a h) (hb : ∀ h, 1 ≤ b h) : 1 ≤ dite p a b := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+@[to_additive]
+lemma dite_le_one [LE α] (ha : ∀ h, a h ≤ 1) (hb : ∀ h, b h ≤ 1) : dite p a b ≤ 1 := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+@[to_additive dite_pos]
+lemma one_lt_dite [LT α] (ha : ∀ h, 1 < a h) (hb : ∀ h, 1 < b h) : 1 < dite p a b := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+@[to_additive]
+lemma dite_lt_one [LT α] (ha : ∀ h, a h < 1) (hb : ∀ h, b h < 1) : dite p a b < 1 := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+end dite
+
+section
+variable [One α] {p : Prop} [Decidable p] {a b : α}
+
+@[to_additive ite_nonneg]
+lemma one_le_ite [LE α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ ite p a b := by split <;> assumption
+
+@[to_additive]
+lemma ite_le_one [LE α] (ha : a ≤ 1) (hb : b ≤ 1) : ite p a b ≤ 1 := by split <;> assumption
+
+@[to_additive ite_pos]
+lemma one_lt_ite [LT α] (ha : 1 < a) (hb : 1 < b) : 1 < ite p a b := by split <;> assumption
+
+@[to_additive]
+lemma ite_lt_one [LT α] (ha : a < 1) (hb : b < 1) : ite p a b < 1 := by split <;> assumption
+
+end

Mathlib/Data/Num/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Lean.Linter.Deprecated
-import Mathlib.Algebra.Group.ZeroOne
+import Mathlib.Data.One.Defs
 import Mathlib.Data.Int.Notation
 import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Tactic.TypeStar

Mathlib/Algebra/Group/ZeroOne.lean renamed to Mathlib/Data/One/Defs.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Neil Strickland
 -/
 import Mathlib.Data.Nat.Defs
 import Mathlib.Data.PNat.Notation
+import Mathlib.Data.One.Defs
 import Mathlib.Order.Basic
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Lift