R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ r, 0 < r ∧ r • x = y
⊢ SameRay R x y
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y
refine' ⟨fun h => _, fun h => h.exists_pos_left hx hy⟩
case intro.intro
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ r, 0 < r ∧ r • x = y
⊢ SameRay R x y
rcases h with ⟨r, hr, rfl⟩
no goals
case intro.intro
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)
exact SameRay.sameRay_pos_smul_right x hr