chore(group_theory/perm/support): support_pow_le over nat (#8225)

Previously, both `support_pow_le` and `support_gpow_le` had the
power as an `int`. Now we properly differentiate the two and avoid
slow defeq checks.

src/group_theory/perm/cycles.lean

@@ -247,14 +247,14 @@ calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
         pow_one, units.neg_mul_neg] }
 using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
 
--- The lemma `support_pow_le` is relevant. It means that `h2` is equivalent to
+-- The lemma `support_gpow_le` is relevant. It means that `h2` is equivalent to
 -- `σ.support = (σ ^ n).support`, as well as to `σ.support.card ≤ (σ ^ n).support.card`.
-lemma is_cycle_of_is_cycle_pow {σ : perm α} {n : ℤ}
+lemma is_cycle_of_is_cycle_gpow {σ : perm α} {n : ℤ}
   (h1 : is_cycle (σ ^ n)) (h2 : σ.support ≤ (σ ^ n).support) : is_cycle σ :=
 begin
   have key : ∀ x : α, (σ ^ n) x ≠ x ↔ σ x ≠ x,
   { simp_rw [←mem_support],
-    exact finset.ext_iff.mp (le_antisymm (support_pow_le σ n) h2) },
+    exact finset.ext_iff.mp (le_antisymm (support_gpow_le σ n) h2) },
   obtain ⟨x, hx1, hx2⟩ := h1,
   refine ⟨x, (key x).mp hx1, λ y hy, _⟩,
   cases (hx2 y ((key y).mpr hy)) with i _,
@@ -763,8 +763,8 @@ begin
   cases exists_pow_eq_self_of_coprime h0 with m hm,
   have h2' : (σ ^ n).support = ⊤ := eq.trans (support_pow_coprime h0) h2,
   have h1' : is_cycle ((σ ^ n) ^ (m : ℤ)) := by rwa ← hm at h1,
-  replace h1' : is_cycle (σ ^ n) := is_cycle_of_is_cycle_pow h1'
-    (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm))),
+  replace h1' : is_cycle (σ ^ n) := is_cycle_of_is_cycle_gpow h1'
+    (le_trans (support_gpow_le σ n) (ge_of_eq (congr_arg support hm))),
   rw [eq_top_iff, ←closure_cycle_adjacent_swap h1' h2' x, closure_le, set.insert_subset],
   exact ⟨subgroup.pow_mem (closure _) (subset_closure (set.mem_insert σ _)) n,
     set.singleton_subset_iff.mpr (subset_closure (set.mem_insert_of_mem _ (set.mem_singleton _)))⟩,

src/group_theory/perm/support.lean

@@ -245,9 +245,9 @@ begin
   { rw [list.prod_cons, mul_apply, ih (λ g hg, hx g (or.inr hg)), hx f (or.inl rfl)] },
 end
 
-lemma support_pow_le (σ : perm α) (n : ℤ) :
+lemma support_pow_le (σ : perm α) (n : ℕ) :
   (σ ^ n).support ≤ σ.support :=
-λ x h1, mem_support.mpr (λ h2, mem_support.mp h1 (gpow_apply_eq_self_of_apply_eq_self h2 n))
+λ x h1, mem_support.mpr (λ h2, mem_support.mp h1 (pow_apply_eq_self_of_apply_eq_self h2 n))
 
 @[simp] lemma support_inv (σ : perm α) : support (σ⁻¹) = σ.support :=
 by simp_rw [finset.ext_iff, mem_support, not_iff_not,
@@ -325,7 +325,7 @@ end
 
 lemma support_gpow_le (σ : perm α) (n : ℤ) :
   (σ ^ n).support ≤ σ.support :=
-by { cases n; exact support_pow_le σ _ }
+λ x h1, mem_support.mpr (λ h2, mem_support.mp h1 (gpow_apply_eq_self_of_apply_eq_self h2 n))
 
 @[simp] lemma support_swap {x y : α} (h : x ≠ y) : support (swap x y) = {x, y} :=
 begin