refactor: Delete Algebra.GroupPower.Lemmas (#9411)

`Algebra.GroupPower.Lemmas` used to be a big bag of lemmas that made it there on the criterion that they needed "more imports". This was completely untrue, as all lemmas could be moved to earlier files in PRs: - #9440 - #9442 - #9443 - #9455 - #9456 - #9457 - #9459 - #9461 - #9463 - #9466 - #9501 - #9502 - #9503 - #9505 - #9551 - #9553 - #9720 - #9739 - #9740 - #9805 - #9806 - and this one There are several reasons for this: * Necessary lemmas have been moved to earlier files since lemmas were dumped in `Algebra.GroupPower.Lemmas` * In the Lean 3 → Lean 4 transition, Std acquired basic `Int` and `Nat` lemmas which let us shortcircuit the part of the algebraic order hierarchy on which the corresponding general lemmas rest * Some proofs were overpowered * Some earlier files were tangled and I have untangled them This PR finishes the job by moving the last few lemmas out of `Algebra.GroupPower.Lemmas`, which is therefore deleted.
leanprover-community · Jan 30, 2024 · 6eb43dc · 6eb43dc
1 parent b977375
commit 6eb43dc
Show file tree

Hide file tree

Showing 24 changed files with 32 additions and 87 deletions.
diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Manuel Candales. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 -/
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Data.Nat.Prime

diff --git a/Mathlib.lean b/Mathlib.lean
@@ -209,7 +209,6 @@ import Mathlib.Algebra.GroupPower.CovariantClass
 import Mathlib.Algebra.GroupPower.Hom
 import Mathlib.Algebra.GroupPower.Identities
 import Mathlib.Algebra.GroupPower.IterateHom
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.GroupPower.NegOnePow
 import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Algebra.GroupPower.Ring

diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Category.MonCat.Basic
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.CategoryTheory.Endomorphism
 
 #align_import algebra.category.Group.basic from "leanprover-community/mathlib"@"524793de15bc4c52ee32d254e7d7867c7176b3af"

diff --git a/Mathlib/Algebra/EuclideanDomain/Instances.lean b/Mathlib/Algebra/EuclideanDomain/Instances.lean
@@ -6,11 +6,8 @@ Authors: Louis Carlin, Mario Carneiro
 import Mathlib.Algebra.EuclideanDomain.Defs
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
-import Mathlib.Algebra.Order.Ring.Lemmas
-import Mathlib.Init.Data.Int.Order
-import Mathlib.Data.Int.Basic
-import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Int.Order.Basic
+import Mathlib.Data.Nat.Order.Basic
 
 #align_import algebra.euclidean_domain.instances from "leanprover-community/mathlib"@"e1bccd6e40ae78370f01659715d3c948716e3b7e"
 

diff --git a/Mathlib/Algebra/GroupPower/CovariantClass.lean b/Mathlib/Algebra/GroupPower/CovariantClass.lean
@@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Robert Y. Lewis, Yury G. Kudryashov
 -/
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.Order.Monoid.OrderDual
-import Mathlib.Data.Nat.Defs
 import Mathlib.Tactic.Monotonicity.Attr
 
 /-!

diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean
diff --git a/Mathlib/Algebra/ModEq.lean b/Mathlib/Algebra/ModEq.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Data.Int.ModEq
 import Mathlib.GroupTheory.QuotientGroup
 

diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.GroupTheory.GroupAction.Group

diff --git a/Mathlib/Algebra/Order/Group/Lattice.lean b/Mathlib/Algebra/Order/Group/Lattice.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Christopher Hoskin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin, Yaël Dillies
 -/
-import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.Order.Group.OrderIso
 
 #align_import algebra.order.lattice_group from "leanprover-community/mathlib"@"5dc275ec639221ca4d5f56938eb966f6ad9bc89f"

diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean
@@ -250,6 +250,20 @@ theorem pow_nonneg (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ a ^ n
     exact mul_nonneg H (pow_nonneg H _)
 #align pow_nonneg pow_nonneg
 
+lemma pow_le_pow_of_le_one (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : ∀ {m n : ℕ}, m ≤ n → a ^ n ≤ a ^ m
+  | _, _, Nat.le.refl => le_rfl
+  | _, _, Nat.le.step h => by
+    rw [pow_succ]
+    exact (mul_le_of_le_one_left (pow_nonneg ha₀ _) ha₁).trans $ pow_le_pow_of_le_one ha₀ ha₁ h
+#align pow_le_pow_of_le_one pow_le_pow_of_le_one
+
+lemma pow_le_of_le_one (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ a :=
+  (pow_one a).subst (pow_le_pow_of_le_one h₀ h₁ (Nat.pos_of_ne_zero hn))
+#align pow_le_of_le_one pow_le_of_le_one
+
+lemma sq_le (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a := pow_le_of_le_one h₀ h₁ two_ne_zero
+#align sq_le sq_le
+
 -- Porting note: it's unfortunate we need to write `(@one_le_two α)` here.
 theorem add_le_mul_two_add (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
   calc
@@ -1048,6 +1062,13 @@ theorem mul_self_inj {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b
   (@strictMonoOn_mul_self α _).eq_iff_eq h1 h2
 #align mul_self_inj mul_self_inj
 
+lemma sign_cases_of_C_mul_pow_nonneg  (h : ∀ n, 0 ≤ a * b ^ n) : a = 0 ∨ 0 < a ∧ 0 ≤ b := by
+  have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0
+  refine this.eq_or_gt.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩
+  simpa only [pow_one] using h 1
+set_option linter.uppercaseLean3 false in
+#align sign_cases_of_C_mul_pow_nonneg sign_cases_of_C_mul_pow_nonneg
+
 variable [ExistsAddOfLE α]
 
 -- See note [lower instance priority]

diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Johannes Hölzl, Yury G. Kudryashov, Patrick Massot
 -/
 import Mathlib.Algebra.GeomSum
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Order.Filter.Archimedean
 import Mathlib.Order.Iterate
 import Mathlib.Topology.Instances.ENNReal

diff --git a/Mathlib/Data/Int/Associated.lean b/Mathlib/Data/Int/Associated.lean
@@ -5,7 +5,6 @@ Authors: Anne Baanen
 -/
 import Mathlib.Algebra.Associated
 import Mathlib.Data.Int.Units
-import Mathlib.Data.Int.Basic
 
 #align_import data.int.associated from "leanprover-community/mathlib"@"207cfac9fcd06138865b5d04f7091e46d9320432"
 /-!

diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
@@ -5,7 +5,6 @@ Authors: Jeremy Avigad
 -/
 import Mathlib.Data.Int.Basic
 import Mathlib.Data.Nat.Bitwise
-import Mathlib.Data.Nat.Pow
 import Mathlib.Data.Nat.Size
 import Mathlib.Init.Data.Int.Bitwise
 

diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean
@@ -241,3 +241,5 @@ Those lemmas have been deprecated on 2023-12-23.
 @[deprecated] protected alias Nat.pow_right_strictMono := pow_right_strictMono
 @[deprecated] alias Nat.pow_le_iff_le_right := pow_le_pow_iff_right
 @[deprecated] alias Nat.pow_lt_iff_lt_right := pow_lt_pow_iff_right
+
+assert_not_exists Set.range
diff --git a/Mathlib/Data/Real/CauSeq.lean b/Mathlib/Data/Real/CauSeq.lean
@@ -1001,3 +1001,5 @@ protected theorem sup_inf_distrib_right (a b c : CauSeq α abs) : a ⊓ b ⊔ c
 end Abs
 
 end CauSeq
+
+assert_not_exists Module
diff --git a/Mathlib/Data/Real/NNReal.lean b/Mathlib/Data/Real/NNReal.lean
@@ -6,7 +6,6 @@ Authors: Johan Commelin
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Algebra.BigOperators.Ring
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Order.Field.Canonical.Basic
 import Mathlib.Algebra.Order.Nonneg.Field
 import Mathlib.Algebra.Order.Nonneg.Floor

diff --git a/Mathlib/Data/ZMod/Quotient.lean b/Mathlib/Data/ZMod/Quotient.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import Mathlib.Algebra.Group.Equiv.TypeTags
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Data.ZMod.Basic
 import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.RingTheory.Ideal.QuotientOperations

diff --git a/Mathlib/Dynamics/Ergodic/AddCircle.lean b/Mathlib/Dynamics/Ergodic/AddCircle.lean
@@ -3,10 +3,11 @@ Copyright (c) 2022 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.MeasureTheory.Group.AddCircle
+import Mathlib.Algebra.Order.Ring.Abs
+import Mathlib.Data.Set.Pointwise.Iterate
 import Mathlib.Dynamics.Ergodic.Ergodic
 import Mathlib.MeasureTheory.Covering.DensityTheorem
-import Mathlib.Data.Set.Pointwise.Iterate
+import Mathlib.MeasureTheory.Group.AddCircle
 import Mathlib.MeasureTheory.Measure.Haar.Unique
 
 #align_import dynamics.ergodic.add_circle from "leanprover-community/mathlib"@"5f6e827d81dfbeb6151d7016586ceeb0099b9655"

diff --git a/Mathlib/GroupTheory/GroupAction/Ring.lean b/Mathlib/GroupTheory/GroupAction/Ring.lean
@@ -39,7 +39,7 @@ instance NonUnitalNonAssocSemiring.nat_isScalarTower [NonUnitalNonAssocSemiring
     · simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]
 #align non_unital_non_assoc_semiring.nat_is_scalar_tower NonUnitalNonAssocSemiring.nat_isScalarTower
 
-/-- Note that `AddGroup.int_smulCommClass` requires stronger assumptions on `α`. -/
+/-- Note that `AddMonoid.int_smulCommClass` requires stronger assumptions on `α`. -/
 instance NonUnitalNonAssocRing.int_smulCommClass [NonUnitalNonAssocRing α] :
     SMulCommClass ℤ α α where
   smul_comm n x y :=

diff --git a/Mathlib/GroupTheory/Subgroup/ZPowers.lean b/Mathlib/GroupTheory/Subgroup/ZPowers.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.Data.Countable.Basic
 import Mathlib.Data.Set.Image

diff --git a/Mathlib/NumberTheory/FLT/Four.lean b/Mathlib/NumberTheory/FLT/Four.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Paul van Wamelen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul van Wamelen
 -/
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.NumberTheory.FLT.Basic
 import Mathlib.NumberTheory.PythagoreanTriples
 import Mathlib.RingTheory.Coprime.Lemmas

diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
@@ -58,7 +58,7 @@ import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.Lint
 import Mathlib.Tactic.MkIffOfInductiveProp
--- NormNum imports `Mathlib.Algebra.GroupPower.Lemmas` and `Mathlib.Algebra.Order.Invertible`
+-- NormNum imports `Algebra.Order.Invertible`, `Data.Int.Basic`, `Data.Nat.Cast.Commute`
 -- import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe

diff --git a/Mathlib/Topology/ContinuousFunction/Algebra.lean b/Mathlib/Topology/ContinuousFunction/Algebra.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Nicolò Cavalleri
 -/
 import Mathlib.Algebra.Algebra.Pi
+import Mathlib.Algebra.Order.Group.Lattice
 import Mathlib.Algebra.Periodic
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Star.StarAlgHom

diff --git a/Mathlib/Topology/Instances/Real.lean b/Mathlib/Topology/Instances/Real.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Periodic
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.Algebra.Star