R : Type u_1
V : Type u_2
V' : Type ?u.160080
P : Type u_3
P' : Type ?u.160086
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
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁) +ᵥ p₂ -ᵥ p₂) (x -ᵥ p₁)
R : Type u_1
V : Type u_2
V' : Type ?u.160080
P : Type u_3
P' : Type ?u.160086
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
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ WSameSide s (t • (x -ᵥ p₁) +ᵥ p₂) x
refine' ⟨p₂, hp₂, p₁, hp₁, _⟩
R : Type u_1
V : Type u_2
V' : Type ?u.160080
P : Type u_3
P' : Type ?u.160086
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
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)
R : Type u_1
V : Type u_2
V' : Type ?u.160080
P : Type u_3
P' : Type ?u.160086
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
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁) +ᵥ p₂ -ᵥ p₂) (x -ᵥ p₁)
rw [vadd_vsub]
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.160080
P : Type u_3
P' : Type ?u.160086
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
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)
exact SameRay.sameRay_nonneg_smul_left _ ht