case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x v₁ v₂ : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ r, 0 ≤ r ∧ r • x = 0

case inr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R x y
hx : x ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
obtain rfl | hy := eq_or_ne y 0
no goals
case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x v₁ v₂ : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ r, 0 ≤ r ∧ r • x = 0
exact ⟨0, le_rfl, zero_smul _ _⟩
no goals
case inr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt