case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.364088
P : Type u_3
P' : Type ?u.364094
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
right✝ : t ≤ 1
⊢ SameRay R (↑(lineMap x z) t -ᵥ x) (z -ᵥ x)
R : Type u_1
V : Type u_2
V' : Type ?u.364088
P : Type u_3
P' : Type ?u.364094
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 (y -ᵥ x) (z -ᵥ x)
rcases h with ⟨t, ⟨ht0, _⟩, rfl⟩
no goals
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.364088
P : Type u_3
P' : Type ?u.364094
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
right✝ : t ≤ 1
⊢ SameRay R (↑(lineMap x z) t -ᵥ x) (z -ᵥ x)
simpa [lineMap_apply] using SameRay.sameRay_nonneg_smul_left (z -ᵥ x) ht0