R : Type u_1
V : Type u_2
V' : Type ?u.518717
P : Type u_3
P' : Type ?u.518723
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ ↑(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
R : Type u_1
V : Type u_2
V' : Type ?u.518717
P : Type u_3
P' : Type ?u.518723
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
refine' ⟨r₁ / r₂, ⟨div_nonneg hr₁ (hr₁.trans hr₂), div_le_one_of_le hr₂ (hr₁.trans hr₂)⟩, _⟩
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.518717
P : Type u_3
P' : Type ?u.518723
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ ↑(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

case neg
R : Type u_1
V : Type u_2
V' : Type ?u.518717
P : Type u_3
P' : Type ?u.518723
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : ¬r₁ = 0
⊢ ↑(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
R : Type u_1
V : Type u_2
V' : Type ?u.518717
P : Type u_3
P' : Type ?u.518723
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ ↑(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
by_cases h : r₁ = 0
no goals
case neg
R : Type u_1
V : Type u_2
V' : Type ?u.518717
P : Type u_3
P' : Type ?u.518723
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : ¬r₁ = 0
⊢ ↑(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
simp [lineMap_apply, smul_smul, ((hr₁.lt_of_ne' h).trans_le hr₂).ne.symm]
no goals
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.518717
P : Type u_3
P' : Type ?u.518723
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ ↑(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
simp [h]