case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
⊢ 0 = 0

case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0

case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h : SameRay R x (r • x)
⊢ x = 0
rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)
no goals
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
⊢ 0 = 0
rfl
no goals
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0
simpa [hr.ne] using h₀
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0
rw [← sub_eq_zero, smul_smul, ← sub_smul, smul_eq_zero] at h
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ r₂ * r < r₁
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
refine' h.resolve_left (ne_of_gt <| sub_pos.2 _)
no goals
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.147146
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ r₂ * r < r₁
exact (mul_neg_of_pos_of_neg hr₂ hr).trans hr₁