R : Type u_2
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type ?u.5473
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.5555
inst✝¹ : DecidableEq ι
x✝ y✝ z : M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y
R : Type u_2
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type ?u.5473
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.5555
inst✝¹ : DecidableEq ι
x✝ y✝ z : M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R x y
rw [Subsingleton.elim x 0]
no goals
R : Type u_2
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type ?u.5473
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.5555
inst✝¹ : DecidableEq ι
x✝ y✝ z : M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y
exact zero_left _