case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.272422
P : Type u_3
P' : Type ?u.272428
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'
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x (↑(lineMap w z) t₁)
⊢ Wbtw R w x z
R : Type u_1
V : Type u_2
V' : Type ?u.272422
P : Type u_3
P' : Type ?u.272428
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'
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R w x z
rcases h₁ with ⟨t₁, ht₁, rfl⟩
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.272422
P : Type u_3
P' : Type ?u.272428
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'
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ Wbtw R w (↑(lineMap w (↑(lineMap w z) t₁)) t₂) z
case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.272422
P : Type u_3
P' : Type ?u.272428
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'
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x (↑(lineMap w z) t₁)
⊢ Wbtw R w x z
rcases h₂ with ⟨t₂, ht₂, rfl⟩
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.272422
P : Type u_3
P' : Type ?u.272428
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'
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ↑(lineMap w z) (t₂ * t₁) = ↑(lineMap w (↑(lineMap w z) t₁)) t₂
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.272422
P : Type u_3
P' : Type ?u.272428
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'
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ Wbtw R w (↑(lineMap w (↑(lineMap w z) t₁)) t₂) z
refine' ⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one ht₂.2 ht₁.1 ht₁.2⟩, _⟩
no goals
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.272422
P : Type u_3
P' : Type ?u.272428
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'
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ↑(lineMap w z) (t₂ * t₁) = ↑(lineMap w (↑(lineMap w z) t₁)) t₂
rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]