case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.489120
P : Type u_3
P' : Type ?u.489126
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
h : Wbtw R x y (↑(lineMap x y) r)
⊢ ↑(lineMap x y) r ∈ affineSpan R {x, y}
R : Type u_1
V : Type u_2
V' : Type ?u.489120
P : Type u_3
P' : Type ?u.489126
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
hne : x ≠ y
⊢ z ∈ affineSpan R {x, y}
rcases h.right_mem_image_Ici_of_left_ne hne with ⟨r, ⟨-, rfl⟩⟩
no goals
case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.489120
P : Type u_3
P' : Type ?u.489126
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
h : Wbtw R x y (↑(lineMap x y) r)
⊢ ↑(lineMap x y) r ∈ affineSpan R {x, y}
exact lineMap_mem_affineSpan_pair _ _ _