Theorem: MvPolynomial.NoZeroSmulDivisors.smul_eq_zero_iff_eq_zero_or_eq_zero (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0
Tactic:
constructor <;> intro h
State after:
case mp
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c • x = 0
⊢ c = 0 ∨ x = 0

case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0

State before:
case mp
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c • x = 0
⊢ c = 0 ∨ x = 0

case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0
Tactic:
exact eq_zero_or_eq_zero_of_smul_eq_zero h
State after:
case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0

State before:
case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0
Tactic:
cases' h with h h <;> simp [h]
State after:
no goals