case intro.intro
G : Type ?u.172795
H : Type ?u.172798
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0
G : Type ?u.172795
H : Type ?u.172798
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
⊢ ∃ n, 0 < n ∧ n • f = 0
obtain ⟨n, npos, hn⟩ := (isOfFinAddOrder_iff_nsmul_eq_zero _).mp (tR 1)
no goals
case intro.intro
G : Type ?u.172795
H : Type ?u.172798
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0
exact ⟨n, npos, by simp only [nsmul_eq_smul_cast R _ f, ← nsmul_one, hn, zero_smul]⟩
no goals
G : Type ?u.172795
H : Type ?u.172798
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ n • f = 0
simp only [nsmul_eq_smul_cast R _ f, ← nsmul_one, hn, zero_smul]