-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsion'_powers_iff (p : R) :
    IsTorsion' M (Submonoid.powers p) ↔ ∀ x : M, ∃ n : ℕ, p ^ n • x = 0

Proof state:
case mpr
R : Type u_1
M : Type u_2
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

Tactic:
let ⟨n, hn⟩ := h x

Result:
case mpr
R : Type u_1
M : Type u_2
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

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ (∀ (x : M), ∃ n, p ^ n • x = 0) → IsTorsion' M ↥(Submonoid.powers p)

Tactic:
intro h x

Result:
case mpr
R : Type u_1
M : Type u_2
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

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ ∃ n, p ^ n • x = 0

Tactic:
use n

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ p ^ n • x = 0

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : (fun x => p ^ x) n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ ∃ n, p ^ n • x = 0

Tactic:
dsimp at hn

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ ∃ n, p ^ n • x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ n, p ^ n • x = 0

Tactic:
constructor

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

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

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
⊢ ∃ n, p ^ n • x = 0

Tactic:
let ⟨⟨a, ⟨n, hn⟩⟩, hx⟩ := @h x

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : (fun x => p ^ x) n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ ∃ n, p ^ n • x = 0

Proof state:
case mpr
R : Type u_1
M : Type u_2
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

Tactic:
exact ⟨⟨_, ⟨n, rfl⟩⟩, hn⟩

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ p ^ n • x = 0

Tactic:
rw [hn]

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ a • x = 0

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

Tactic:
intro h x

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
⊢ ∃ n, p ^ n • x = 0

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ a • x = 0

Tactic:
apply hx

Result:
no goals