[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
r : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
⊢ ∀ {c : R} {x : M × N}, c • x = 0 → c = 0 ∨ x = 0
[PROOFSTEP]
intro c ⟨x, y⟩ h
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
r : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
c : R
x : M
y : N
h : c • (x, y) = 0
⊢ c = 0 ∨ (x, y) = 0
[PROOFSTEP]
exact
  or_iff_not_imp_left.mpr fun hc =>
    mk.inj_iff.mpr
      ⟨(smul_eq_zero.mp (congr_arg fst h)).resolve_left hc, (smul_eq_zero.mp (congr_arg snd h)).resolve_left hc⟩
