R : Type u_3
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_2
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ x ∈ ⊤
R : Type u_3
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_2
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ ∃ a, a • x = 0
rw [← @mem_torsion'_iff R, h]
no goals
R : Type u_3
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_2
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ x ∈ ⊤
trivial