case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.367054
P : Type u_3
P' : Type ?u.367060
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
left✝ : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (z -ᵥ x) (z -ᵥ ↑(lineMap x z) t)
R : Type u_1
V : Type u_2
V' : Type ?u.367054
P : Type u_3
P' : Type ?u.367060
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (z -ᵥ x) (z -ᵥ y)
rcases h with ⟨t, ⟨_, ht1⟩, rfl⟩
no goals
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.367054
P : Type u_3
P' : Type ?u.367060
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
left✝ : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (z -ᵥ x) (z -ᵥ ↑(lineMap x z) t)
simpa [lineMap_apply, vsub_vadd_eq_vsub_sub, sub_smul] using
  SameRay.sameRay_nonneg_smul_right (z -ᵥ x) (sub_nonneg.2 ht1)