α : Type ?u.271530
R : Type ?u.271533
k : Type ?u.271536
S : Type ?u.271539
M : Type u_1
M₂ : Type ?u.271545
M₃ : Type ?u.271548
ι : Type ?u.271551
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
c : ℕ
x : M
⊢ c • x = 0 → c = 0 ∨ x = 0
α : Type ?u.271530
R : Type ?u.271533
k : Type ?u.271536
S : Type ?u.271539
M : Type u_1
M₂ : Type ?u.271545
M₃ : Type ?u.271548
ι : Type ?u.271551
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
⊢ ∀ {c : ℕ} {x : M}, c • x = 0 → c = 0 ∨ x = 0
intro c x
α : Type ?u.271530
R : Type ?u.271533
k : Type ?u.271536
S : Type ?u.271539
M : Type u_1
M₂ : Type ?u.271545
M₃ : Type ?u.271548
ι : Type ?u.271551
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
c : ℕ
x : M
⊢ ↑c = 0 ∨ x = 0 → c = 0 ∨ x = 0
α : Type ?u.271530
R : Type ?u.271533
k : Type ?u.271536
S : Type ?u.271539
M : Type u_1
M₂ : Type ?u.271545
M₃ : Type ?u.271548
ι : Type ?u.271551
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
c : ℕ
x : M
⊢ c • x = 0 → c = 0 ∨ x = 0
rw [nsmul_eq_smul_cast R, smul_eq_zero]
no goals
α : Type ?u.271530
R : Type ?u.271533
k : Type ?u.271536
S : Type ?u.271539
M : Type u_1
M₂ : Type ?u.271545
M₃ : Type ?u.271548
ι : Type ?u.271551
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
c : ℕ
x : M
⊢ ↑c = 0 ∨ x = 0 → c = 0 ∨ x = 0
simp