case h
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) ↔ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
inst✝ : Group N
x : G
⊢ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
ext y
case h.mp
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
inst✝ : Group N
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
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x)) → y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x)
case h
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) ↔ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
constructor
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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))
case h.mp
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) → y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
rintro ⟨z, ⟨m, hm⟩, hz2⟩
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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))
use m
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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
simp only at *
no goals
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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
rwa [← ofMul_zpow, hm]
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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)
case h.mpr
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x)) → y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x)
rintro ⟨n, hn⟩
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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)
refine' ⟨x ^ n, ⟨n, rfl⟩, _⟩
no goals
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type ?u.32458
inst✝¹ : AddGroup A
N : Type ?u.32464
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
rwa [ofMul_zpow]