R : Type u_1
V : Type u_2
V' : Type ?u.114846
P : Type u_3
P' : Type ?u.114852
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R (x -ᵥ x) (y -ᵥ x)
R : Type u_1
V : Type u_2
V' : Type ?u.114846
P : Type u_3
P' : Type ?u.114852
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ WSameSide s x y
refine' ⟨x, hx, x, hx, _⟩
R : Type u_1
V : Type u_2
V' : Type ?u.114846
P : Type u_3
P' : Type ?u.114852
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R 0 (y -ᵥ x)
R : Type u_1
V : Type u_2
V' : Type ?u.114846
P : Type u_3
P' : Type ?u.114852
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R (x -ᵥ x) (y -ᵥ x)
rw [vsub_self]
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.114846
P : Type u_3
P' : Type ?u.114852
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R 0 (y -ᵥ x)
apply SameRay.zero_left