𝕜 : Type u_1
E : Type u_2
F : Type ?u.153306
G : Type ?u.153309
ι : Type ?u.153312
π : ι → Type ?u.153317
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ (fun θ => y + θ • (z - y)) '' Icc 0 1
⊢ SameRay 𝕜 (x - y) (z - x)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.153306
G : Type ?u.153309
ι : Type ?u.153312
π : ι → Type ?u.153317
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ [y-[𝕜]z]
⊢ SameRay 𝕜 (x - y) (z - x)
rw [segment_eq_image'] at h
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.153306
G : Type ?u.153309
ι : Type ?u.153312
π : ι → Type ?u.153317
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
θ : 𝕜
hθ₀ : 0 ≤ θ
hθ₁ : θ ≤ 1
⊢ SameRay 𝕜 ((fun θ => y + θ • (z - y)) θ - y) (z - (fun θ => y + θ • (z - y)) θ)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.153306
G : Type ?u.153309
ι : Type ?u.153312
π : ι → Type ?u.153317
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ (fun θ => y + θ • (z - y)) '' Icc 0 1
⊢ SameRay 𝕜 (x - y) (z - x)
rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩
no goals
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.153306
G : Type ?u.153309
ι : Type ?u.153312
π : ι → Type ?u.153317
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
θ : 𝕜
hθ₀ : 0 ≤ θ
hθ₁ : θ ≤ 1
⊢ SameRay 𝕜 ((fun θ => y + θ • (z - y)) θ - y) (z - (fun θ => y + θ • (z - y)) θ)
simpa only [add_sub_cancel', ← sub_sub, sub_smul, one_smul] using
  (SameRay.sameRay_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)