[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
⊢ zpowers g = closure {g}
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}
[PROOFSTEP]
exact mem_closure_singleton.symm
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
N : Type u_3
inst✝¹ : Group N
R : Type u_4
inst✝ : Ring R
r : R
k : ℤ
⊢ ↑k * r ∈ zmultiples r
[PROOFSTEP]
simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
N : Type u_3
inst✝¹ : Group N
R : Type u_4
inst✝ : Ring R
r : R
k : ℤ
⊢ (fun x => x • 1) k = ↑k
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝³ : Group G
A✝ : Type u_2
inst✝² : AddGroup A✝
N : Type u_3
inst✝¹ : Group N
A : Type u_4
inst✝ : AddGroupWithOne A
⊢ AddMonoidHom.range (castAddHom A) = AddSubgroup.zmultiples 1
[PROOFSTEP]
ext a
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
A✝ : Type u_2
inst✝² : AddGroup A✝
N : Type u_3
inst✝¹ : Group N
A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ a ∈ AddMonoidHom.range (castAddHom A) ↔ a ∈ AddSubgroup.zmultiples 1
[PROOFSTEP]
simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (↑f x)
[PROOFSTEP]
rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
a b k : ℤ
⊢ (fun x => x • a) k = b ↔ b = a * k
[PROOFSTEP]
rw [mul_comm, eq_comm, ← smul_eq_mul]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
⊢ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
ext y
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) ↔ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) → y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
rintro ⟨z, ⟨m, hm⟩, hz2⟩
[GOAL]
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
z : G
hz2 : ↑Additive.ofMul z = y
m : ℤ
hm : (fun x x_1 => x ^ x_1) x m = z
⊢ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
use m
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
z : G
hz2 : ↑Additive.ofMul z = y
m : ℤ
hm : (fun x x_1 => x ^ x_1) x m = z
⊢ (fun x_1 => x_1 • ↑Additive.ofMul x) m = y
[PROOFSTEP]
simp only at *
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
z : G
hz2 : ↑Additive.ofMul z = y
m : ℤ
hm : x ^ m = z
⊢ m • ↑Additive.ofMul x = y
[PROOFSTEP]
rwa [← ofMul_zpow, hm]
[GOAL]
case h.mpr
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x)) → y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x)
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • ↑Additive.ofMul x) n = y
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x)
[PROOFSTEP]
refine' ⟨x ^ n, ⟨n, rfl⟩, _⟩
[GOAL]
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • ↑Additive.ofMul x) n = y
⊢ ↑Additive.ofMul (x ^ n) = y
[PROOFSTEP]
rwa [ofMul_zpow]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : A
⊢ ↑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (↑Multiplicative.ofAdd x))
[PROOFSTEP]
symm
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : A
⊢ ↑(Subgroup.zpowers (↑Multiplicative.ofAdd x)) = ↑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)
[PROOFSTEP]
rw [Equiv.eq_image_iff_symm_image_eq]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : A
⊢ ↑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (↑Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)
[PROOFSTEP]
exact ofMul_image_zpowers_eq_zmultiples_ofMul
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g✝ g : G
x✝¹ x✝ : { x // x ∈ zpowers g }
val✝¹ : G
w✝¹ : ℤ
h₁ : (fun x x_1 => x ^ x_1) g w✝¹ = val✝¹
val✝ : G
w✝ : ℤ
h₂ : (fun x x_1 => x ^ x_1) g w✝ = val✝
⊢ { val := val✝¹, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝¹) } *
      { val := val✝, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝) } =
    { val := val✝, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝) } *
      { val := val✝¹, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝¹) }
[PROOFSTEP]
rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← h₁, ← h₂, zpow_mul_comm]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g✝ g : G
H : Subgroup G
⊢ zpowers g ≤ H ↔ g ∈ H
[PROOFSTEP]
rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g✝ g : G
⊢ zpowers g = ⊥ ↔ g = 1
[PROOFSTEP]
rw [eq_bot_iff, zpowers_le, mem_bot]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g : G
S : Set G
hS : closure S = ⊤
⊢ center G = ⨅ (g : G) (_ : g ∈ S), centralizer ↑(zpowers g)
[PROOFSTEP]
rw [← centralizer_univ, ← coe_top, ← hS, centralizer_closure]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g : G
S : Set G
hS : closure S = ⊤
⊢ center G = ⨅ (g : ↑S), centralizer ↑(zpowers ↑g)
[PROOFSTEP]
rw [center_eq_iInf S hS, ← iInf_subtype'']
