[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ g • s = s
[PROOFSTEP]
suffices ∀ {g' : G} (_ : g' ^ n ^ j = 1), g' • s ⊆ s
  by
  refine' le_antisymm (this hg) _
  conv_lhs => rw [← smul_inv_smul g s]
  replace hg : g⁻¹ ^ n ^ j = 1
  · rw [inv_zpow, hg, inv_one]
  simpa only [le_eq_subset, set_smul_subset_set_smul_iff] using this hg
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • s = s
[PROOFSTEP]
refine' le_antisymm (this hg) _
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ s ≤ g • s
[PROOFSTEP]
conv_lhs => rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s
[PROOFSTEP]
rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s
[PROOFSTEP]
rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s
[PROOFSTEP]
rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • g⁻¹ • s ≤ g • s
[PROOFSTEP]
replace hg : g⁻¹ ^ n ^ j = 1
[GOAL]
case hg
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g⁻¹ ^ n ^ j = 1
[PROOFSTEP]
rw [inv_zpow, hg, inv_one]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
hg : g⁻¹ ^ n ^ j = 1
⊢ g • g⁻¹ • s ≤ g • s
[PROOFSTEP]
simpa only [le_eq_subset, set_smul_subset_set_smul_iff] using this hg
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
[PROOFSTEP]
rw [(IsFixedPt.preimage_iterate hs j : (zpowGroupHom n)^[j] ⁻¹' s = s).symm]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ ∀ {g' : G}, g' ^ n ^ j = 1 → g' • (fun x => x ^ n)^[j] ⁻¹' s ⊆ (fun x => x ^ n)^[j] ⁻¹' s
[PROOFSTEP]
rintro g' hg' - ⟨y, hy, rfl⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
⊢ (fun x => g' • x) y ∈ (fun x => x ^ n)^[j] ⁻¹' s
[PROOFSTEP]
change (zpowGroupHom n)^[j] (g' * y) ∈ s
[GOAL]
case intro.intro
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
⊢ (↑(zpowGroupHom n))^[j] (g' * y) ∈ s
[PROOFSTEP]
replace hg' : (zpowGroupHom n)^[j] g' = 1
[GOAL]
case hg'
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
⊢ (↑(zpowGroupHom n))^[j] g' = 1
[PROOFSTEP]
simpa [zpowGroupHom]
[GOAL]
case intro.intro
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
hg' : (↑(zpowGroupHom n))^[j] g' = 1
⊢ (↑(zpowGroupHom n))^[j] (g' * y) ∈ s
[PROOFSTEP]
rwa [iterate_map_mul, hg', one_mul]
