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
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
rw [(IsFixedPt.preimage_iterate hs j : zpowGroupHom n^[j] ⁻¹' s = s).symm]
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
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
rintro g' hg' - ⟨y, hy, rfl⟩
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
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
change (zpowGroupHom n^[j]) (g' * y) ∈ s
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

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
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
replace hg' : (zpowGroupHom n^[j]) g' = 1
no goals
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
rwa [MonoidHom.iterate_map_mul, hg', one_mul]
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
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
refine' le_antisymm (this 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 • g⁻¹ • s ≤ g • s
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
conv_lhs => rw [← smul_inv_smul g s]
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

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
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
replace hg : g⁻¹ ^ n ^ j = 1
no goals
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
simpa only [le_eq_subset, set_smul_subset_set_smul_iff] using this hg
no goals
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
rw [inv_zpow, hg, inv_one]
no goals
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
simpa [zpowGroupHom]