case mp
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0

case mpr
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ 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
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0
constructor
case mp.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
⊢ SameRay R x (r • x) ∧ r • x ≠ 0
case mp
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0
rintro ⟨r, hr, rfl⟩
no goals
case mp.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
⊢ SameRay R x (r • x) ∧ r • x ≠ 0
simp [hx, hr.le, hr.ne']
case mpr.intro
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ r, 0 < r ∧ r • x = y
case mpr
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y
rintro ⟨hxy, hy⟩
no goals
case mpr.intro
R : Type u_2
inst✝² : LinearOrderedField R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ r, 0 < r ∧ r • x = y
exact (exists_pos_left_iff_sameRay hx hy).2 hxy