case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M { x // x ∈ Submonoid.powers p } → ∀ (x : M), ∃ n, p ^ n • x = 0

case mpr
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ (∀ (x : M), ∃ n, p ^ n • x = 0) → IsTorsion' M { x // x ∈ Submonoid.powers p }
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M { x // x ∈ Submonoid.powers p } ↔ ∀ (x : M), ∃ n, p ^ n • x = 0
constructor
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
⊢ ∃ n, p ^ n • x = 0
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M { x // x ∈ Submonoid.powers p } → ∀ (x : M), ∃ n, p ^ n • x = 0
intro h x
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : (fun x x_1 => x ^ x_1) p n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ ∃ n, p ^ n • x = 0
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
⊢ ∃ n, p ^ n • x = 0
let ⟨⟨a, ⟨n, hn⟩⟩, hx⟩ := @h x
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ ∃ n, p ^ n • x = 0
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : (fun x x_1 => x ^ x_1) p n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ ∃ n, p ^ n • x = 0
dsimp at hn
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ p ^ n • x = 0
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ ∃ n, p ^ n • x = 0
use n
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ a • x = 0
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ p ^ n • x = 0
rw [hn]
no goals
case mp
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ a • x = 0
apply hx
case mpr
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : ∀ (x : M), ∃ n, p ^ n • x = 0
x : M
⊢ ∃ a, a • x = 0
case mpr
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ (∀ (x : M), ∃ n, p ^ n • x = 0) → IsTorsion' M { x // x ∈ Submonoid.powers p }
intro h x
case mpr
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : ∀ (x : M), ∃ n, p ^ n • x = 0
x : M
n : ℕ
hn : p ^ n • x = 0
⊢ ∃ a, a • x = 0
case mpr
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : ∀ (x : M), ∃ n, p ^ n • x = 0
x : M
⊢ ∃ a, a • x = 0
let ⟨n, hn⟩ := h x
no goals
case mpr
R : Type u_2
M : Type u_1
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : ∀ (x : M), ∃ n, p ^ n • x = 0
x : M
n : ℕ
hn : p ^ n • x = 0
⊢ ∃ a, a • x = 0
exact ⟨⟨_, ⟨n, rfl⟩⟩, hn⟩