feat: Induction principle for powers (#3278)

leanprover-community/mathlib3#18668

* [`algebra.group_power.lemmas`@`05101c3df9d9cfe9430edc205860c79b6d660102`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_power/lemmas?range=05101c3df9d9cfe9430edc205860c79b6d660102..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`group_theory.submonoid.membership`@`2ec920d35348cb2d13ac0e1a2ad9df0fdf1a76b4`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/submonoid/membership?range=2ec920d35348cb2d13ac0e1a2ad9df0fdf1a76b4..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`group_theory.subgroup.zpowers`@`f93c11933efbc3c2f0299e47b8ff83e9b539cbf6`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/subgroup/zpowers?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`group_theory.subgroup.pointwise`@`c10e724be91096453ee3db13862b9fb9a992fef2`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/subgroup/pointwise?range=c10e724be91096453ee3db13862b9fb9a992fef2..e655e4ea5c6d02854696f97494997ba4c31be802)
* [`ring_theory.int.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`e655e4ea5c6d02854696f97494997ba4c31be802`](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/int/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..e655e4ea5c6d02854696f97494997ba4c31be802)

Author: YaelDillies

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 
 ! This file was ported from Lean 3 source module algebra.group_power.lemmas
-! leanprover-community/mathlib commit 05101c3df9d9cfe9430edc205860c79b6d660102
+! leanprover-community/mathlib commit e655e4ea5c6d02854696f97494997ba4c31be802
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -271,6 +271,40 @@ theorem zpow_bit1 (a : G) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a := by
 
 end bit1
 
+/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
+by `g` and `g⁻¹` on the left. For subgroups generated by more than one element, see
+`Subgroup.closure_induction_left`. -/
+@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
+addition by `g` and `-g` on the left. For additive subgroups generated by more than one element, see
+`AddSubgroup.closure_induction_left`."]
+theorem zpow_induction_left {g : G} {P : G → Prop} (h_one : P (1 : G))
+    (h_mul : ∀ a, P a → P (g * a)) (h_inv : ∀ a, P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n) := by
+  induction' n using Int.induction_on with n ih n ih
+  · rwa [zpow_zero]
+  · rw [add_comm, zpow_add, zpow_one]
+    exact h_mul _ ih
+  · rw [sub_eq_add_neg, add_comm, zpow_add, zpow_neg_one]
+    exact h_inv _ ih
+#align zpow_induction_left zpow_induction_left
+#align zsmul_induction_left zsmul_induction_left
+
+/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
+by `g` and `g⁻¹` on the right. For subgroups generated by more than one element, see
+`Subgroup.closure_induction_right`. -/
+@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
+addition by `g` and `-g` on the right. For additive subgroups generated by more than one element,
+see `AddSubgroup.closure_induction_right`."]
+theorem zpow_induction_right {g : G} {P : G → Prop} (h_one : P (1 : G))
+    (h_mul : ∀ a, P a → P (a * g)) (h_inv : ∀ a, P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n) := by
+  induction' n using Int.induction_on with n ih n ih
+  · rwa [zpow_zero]
+  · rw [zpow_add_one]
+    exact h_mul _ ih
+  · rw [zpow_sub_one]
+    exact h_inv _ ih
+#align zpow_induction_right zpow_induction_right
+#align zsmul_induction_right zsmul_induction_right
+
 end Group
 
 /-!

Mathlib/GroupTheory/Subgroup/Pointwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module group_theory.subgroup.pointwise
-! leanprover-community/mathlib commit c10e724be91096453ee3db13862b9fb9a992fef2
+! leanprover-community/mathlib commit e655e4ea5c6d02854696f97494997ba4c31be802
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -66,7 +66,9 @@ theorem closure_toSubmonoid (S : Set G) :
 #align subgroup.closure_to_submonoid Subgroup.closure_toSubmonoid
 #align add_subgroup.closure_to_add_submonoid AddSubgroup.closure_toAddSubmonoid
 
-@[to_additive]
+/-- For subgroups generated by a single element, see the simpler `zpow_induction_left`. -/
+@[to_additive "For additive subgroups generated by a single element, see the simpler
+`zsmul_induction_left`."]
 theorem closure_induction_left {p : G → Prop} {x : G} (h : x ∈ closure s) (H1 : p 1)
     (Hmul : ∀ x ∈ s, ∀ (y), p y → p (x * y)) (Hinv : ∀ x ∈ s, ∀ (y), p y → p (x⁻¹ * y)) : p x :=
   let key := (closure_toSubmonoid s).le
@@ -75,7 +77,9 @@ theorem closure_induction_left {p : G → Prop} {x : G} (h : x ∈ closure s) (H
 #align subgroup.closure_induction_left Subgroup.closure_induction_left
 #align add_subgroup.closure_induction_left AddSubgroup.closure_induction_left
 
-@[to_additive]
+/-- For subgroups generated by a single element, see the simpler `zpow_induction_right`. -/
+@[to_additive "For additive subgroups generated by a single element, see the simpler
+`zsmul_induction_right`."]
 theorem closure_induction_right {p : G → Prop} {x : G} (h : x ∈ closure s) (H1 : p 1)
     (Hmul : ∀ (x), ∀ y ∈ s, p x → p (x * y)) (Hinv : ∀ (x), ∀ y ∈ s, p x → p (x * y⁻¹)) : p x :=
   let key := (closure_toSubmonoid s).le

Mathlib/GroupTheory/Subgroup/Zpowers.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module group_theory.subgroup.zpowers
-! leanprover-community/mathlib commit f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
+! leanprover-community/mathlib commit e655e4ea5c6d02854696f97494997ba4c31be802
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -36,6 +36,10 @@ theorem mem_zpowers (g : G) : g ∈ zpowers g :=
   ⟨1, zpow_one _⟩
 #align subgroup.mem_zpowers Subgroup.mem_zpowers
 
+theorem coe_zpowers (g : G) : ↑(zpowers g) = Set.range (g ^ · : ℤ → G) :=
+  rfl
+#align subgroup.coe_zpowers Subgroup.coe_zpowers
+
 theorem zpowers_eq_closure (g : G) : zpowers g = closure {g} := by
   ext
   exact mem_closure_singleton.symm
@@ -45,11 +49,6 @@ theorem range_zpowersHom (g : G) : (zpowersHom G g).range = zpowers g :=
   rfl
 #align subgroup.range_zpowers_hom Subgroup.range_zpowersHom
 
-theorem zpowers_subset {a : G} {K : Subgroup G} (h : a ∈ K) : zpowers a ≤ K := fun x hx =>
-  match x, hx with
-  | _, ⟨i, rfl⟩ => K.zpow_mem h i
-#align subgroup.zpowers_subset Subgroup.zpowers_subset
-
 theorem mem_zpowers_iff {g h : G} : h ∈ zpowers g ↔ ∃ k : ℤ, g ^ k = h :=
   Iff.rfl
 #align subgroup.mem_zpowers_iff Subgroup.mem_zpowers_iff
@@ -100,15 +99,14 @@ attribute [to_additive existing AddSubgroup.zmultiples] Subgroup.zpowers
 attribute [to_additive (attr := simp) AddSubgroup.mem_zmultiples] Subgroup.mem_zpowers
 #align add_subgroup.mem_zmultiples AddSubgroup.mem_zmultiples
 
+attribute [to_additive (attr := norm_cast) AddSubgroup.coe_zmultiples] Subgroup.coe_zpowers
+
 attribute [to_additive AddSubgroup.zmultiples_eq_closure] Subgroup.zpowers_eq_closure
 #align add_subgroup.zmultiples_eq_closure AddSubgroup.zmultiples_eq_closure
 
 attribute [to_additive existing (attr := simp) AddSubgroup.range_zmultiplesHom]
   Subgroup.range_zpowersHom
 
-attribute [to_additive AddSubgroup.zmultiples_subset] Subgroup.zpowers_subset
-#align add_subgroup.zmultiples_subset AddSubgroup.zmultiples_subset
-
 attribute [to_additive AddSubgroup.mem_zmultiples_iff] Subgroup.mem_zpowers_iff
 #align add_subgroup.mem_zmultiples_iff AddSubgroup.mem_zmultiples_iff
 
@@ -187,6 +185,8 @@ theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {x : A} :
 
 namespace Subgroup
 
+variable {s : Set G} {g : G}
+
 @[to_additive zmultiples_isCommutative]
 instance zpowers_isCommutative (g : G) : (zpowers g).IsCommutative :=
   ⟨⟨fun ⟨_, _, h₁⟩ ⟨_, _, h₂⟩ => by
@@ -201,11 +201,25 @@ theorem zpowers_le {g : G} {H : Subgroup G} : zpowers g ≤ H ↔ g ∈ H := by
 #align subgroup.zpowers_le Subgroup.zpowers_le
 #align add_subgroup.zmultiples_le AddSubgroup.zmultiples_le
 
+alias zpowers_le ↔ _ zpowers_le_of_mem
+#align subgroup.zpowers_le_of_mem Subgroup.zpowers_le_of_mem
+
+alias AddSubgroup.zmultiples_le ↔ _ _root_.AddSubgroup.zmultiples_le_of_mem
+#align add_subgroup.zmultiples_le_of_mem AddSubgroup.zmultiples_le_of_mem
+
+attribute [to_additive existing zmultiples_le_of_mem] zpowers_le_of_mem
+
 @[to_additive (attr := simp) zmultiples_eq_bot]
 theorem zpowers_eq_bot {g : G} : zpowers g = ⊥ ↔ g = 1 := by rw [eq_bot_iff, zpowers_le, mem_bot]
 #align subgroup.zpowers_eq_bot Subgroup.zpowers_eq_bot
 #align add_subgroup.zmultiples_eq_bot AddSubgroup.zmultiples_eq_bot
 
+@[to_additive zmultiples_ne_bot]
+theorem zpowers_ne_bot : zpowers g ≠ ⊥ ↔ g ≠ 1 :=
+  zpowers_eq_bot.not
+#align subgroup.zpowers_ne_bot Subgroup.zpowers_ne_bot
+#align add_subgroup.zmultiples_ne_bot AddSubgroup.zmultiples_ne_bot
+
 @[to_additive (attr := simp) zmultiples_zero_eq_bot]
 theorem zpowers_one_eq_bot : Subgroup.zpowers (1 : G) = ⊥ :=
   Subgroup.zpowers_eq_bot.mpr rfl

Mathlib/GroupTheory/Submonoid/Membership.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module group_theory.submonoid.membership
-! leanprover-community/mathlib commit 2ec920d35348cb2d13ac0e1a2ad9df0fdf1a76b4
+! leanprover-community/mathlib commit e655e4ea5c6d02854696f97494997ba4c31be802
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -438,6 +438,10 @@ theorem mem_powers (n : M) : n ∈ powers n :=
   ⟨1, pow_one _⟩
 #align submonoid.mem_powers Submonoid.mem_powers
 
+theorem coe_powers (x : M) : ↑(powers x) = Set.range fun n : ℕ => x ^ n :=
+  rfl
+#align submonoid.coe_powers Submonoid.coe_powers
+
 theorem mem_powers_iff (x z : M) : x ∈ powers z ↔ ∃ n : ℕ, z ^ n = x :=
   Iff.rfl
 #align submonoid.mem_powers_iff Submonoid.mem_powers_iff
@@ -620,6 +624,9 @@ attribute [to_additive existing multiples] Submonoid.powers
 attribute [to_additive (attr := simp) mem_multiples] Submonoid.mem_powers
 #align add_submonoid.mem_multiples AddSubmonoid.mem_multiples
 
+attribute [to_additive (attr := norm_cast) coe_multiples] Submonoid.coe_powers
+#align add_submonoid.coe_multiples AddSubmonoid.coe_multiples
+
 attribute [to_additive mem_multiples_iff] Submonoid.mem_powers_iff
 #align add_submonoid.mem_multiples_iff AddSubmonoid.mem_multiples_iff
 

Mathlib/RingTheory/Int/Basic.lean

@@ -385,8 +385,8 @@ namespace Int
 
 theorem zmultiples_natAbs (a : ℤ) :
     AddSubgroup.zmultiples (a.natAbs : ℤ) = AddSubgroup.zmultiples a :=
-  le_antisymm (AddSubgroup.zmultiples_subset (mem_zmultiples_iff.mpr (dvd_natAbs.mpr (dvd_refl a))))
-    (AddSubgroup.zmultiples_subset (mem_zmultiples_iff.mpr (natAbs_dvd.mpr (dvd_refl a))))
+  le_antisymm (AddSubgroup.zmultiples_le_of_mem (mem_zmultiples_iff.mpr (dvd_natAbs.mpr dvd_rfl)))
+    (AddSubgroup.zmultiples_le_of_mem (mem_zmultiples_iff.mpr (natAbs_dvd.mpr dvd_rfl)))
 #align int.zmultiples_nat_abs Int.zmultiples_natAbs
 
 theorem span_natAbs (a : ℤ) : Ideal.span ({(a.natAbs : ℤ)} : Set ℤ) = Ideal.span {a} := by