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