-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem ofMul_image_zpowers_eq_zmultiples_ofMul {x : G} :
    Additive.ofMul '' (Subgroup.zpowers x : Set G) = AddSubgroup.zmultiples (Additive.ofMul x)

Proof state:
case h.mp
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
⊢ y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) → y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Tactic:
rintro ⟨z, ⟨m, hm⟩, hz2⟩

Result:
case h.mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
z : G
hz2 : Additive.ofMul z = y
m : ℤ
hm : (fun x_1 => x ^ x_1) m = z
⊢ y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Proof state:
G : Type u_1
inst✝ : Group G
x : G
⊢ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Tactic:
ext y

Result:
case h
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
⊢ y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) ↔ y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Proof state:
case h.mpr
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
⊢ y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x)) → y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x)

Tactic:
rintro ⟨n, hn⟩

Result:
case h.mpr.intro
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • Additive.ofMul x) n = y
⊢ y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x)

Proof state:
case h.mpr.intro
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • Additive.ofMul x) n = y
⊢ Additive.ofMul (x ^ n) = y

Tactic:
rwa [ofMul_zpow]

Result:
no goals

Proof state:
case h.mpr.intro
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • Additive.ofMul x) n = y
⊢ y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x)

Tactic:
refine ⟨x ^ n, ⟨n, rfl⟩, ?_⟩

Result:
case h.mpr.intro
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • Additive.ofMul x) n = y
⊢ Additive.ofMul (x ^ n) = y

Proof state:
case h
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
⊢ y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) ↔ y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Tactic:
constructor

Result:
case h.mp
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
⊢ y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) → y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x))

case h.mpr
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
⊢ y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x)) → y ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x)

Proof state:
case h.mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
z : G
hz2 : Additive.ofMul z = y
m : ℤ
hm : (fun x_1 => x ^ x_1) m = z
⊢ y ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Tactic:
use m

Result:
case h
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
z : G
hz2 : Additive.ofMul z = y
m : ℤ
hm : (fun x_1 => x ^ x_1) m = z
⊢ (fun x_1 => x_1 • Additive.ofMul x) m = y

Proof state:
case h
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
z : G
hz2 : Additive.ofMul z = y
m : ℤ
hm : x ^ m = z
⊢ m • Additive.ofMul x = y

Tactic:
rwa [← ofMul_zpow, hm]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
z : G
hz2 : Additive.ofMul z = y
m : ℤ
hm : (fun x_1 => x ^ x_1) m = z
⊢ (fun x_1 => x_1 • Additive.ofMul x) m = y

Tactic:
simp only at *

Result:
case h
G : Type u_1
inst✝ : Group G
x : G
y : Additive G
z : G
hz2 : Additive.ofMul z = y
m : ℤ
hm : x ^ m = z
⊢ m • Additive.ofMul x = y