case h
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x) ↔ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
⊢ ↑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
ext
case h.mp
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x) → x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))

case h.mpr
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x)) → x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x)
case h
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x) ↔ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
constructor
case h.mp.intro.intro.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : ↑Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x x_1 => x ^ x_1) x n = y
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
case h.mp
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x) → x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
rintro ⟨y, ⟨n, hy1⟩, hy2⟩
case h.mp.intro.intro.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : ↑Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x x_1 => x ^ x_1) x n = y
⊢ (fun i => i • ↑Additive.ofMul x) n = x✝
case h.mp.intro.intro.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : ↑Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x x_1 => x ^ x_1) x n = y
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
use n
no goals
case h.mp.intro.intro.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : ↑Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x x_1 => x ^ x_1) x n = y
⊢ (fun i => i • ↑Additive.ofMul x) n = x✝
simpa [← ofMul_pow, hy1]
case h.mpr.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • ↑Additive.ofMul x) n = x✝
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x)
case h.mpr
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x)) → x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x)
rintro ⟨n, hn⟩
case h.mpr.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • ↑Additive.ofMul x) n = x✝
⊢ ↑Additive.ofMul (x ^ n) = x✝
case h.mpr.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • ↑Additive.ofMul x) n = x✝
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x)
refine' ⟨x ^ n, ⟨n, rfl⟩, _⟩
no goals
case h.mpr.intro
M : Type u_1
A : Type ?u.284676
B : Type ?u.284679
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • ↑Additive.ofMul x) n = x✝
⊢ ↑Additive.ofMul (x ^ n) = x✝
rwa [ofMul_pow]