case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.198200
P : Type u_3
P' : Type ?u.198206
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 z : P
hx : x ∈ s
t : R
ht0 : 0 ≤ t
⊢ WSameSide s (↑(lineMap x z) t) z
R : Type u_1
V : Type u_2
V' : Type ?u.198200
P : Type u_3
P' : Type ?u.198206
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 z : P
h : Wbtw R x y z
hx : x ∈ s
⊢ WSameSide s y z
rcases h with ⟨t, ⟨ht0, -⟩, rfl⟩
no goals
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.198200
P : Type u_3
P' : Type ?u.198206
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 z : P
hx : x ∈ s
t : R
ht0 : 0 ≤ t
⊢ WSameSide s (↑(lineMap x z) t) z
exact wSameSide_lineMap_left z hx ht0