case pos
R : Type u_1
V : Type u_2
V' : Type ?u.236526
P : Type u_3
P' : Type ?u.236532
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'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R x (↑(lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1

case neg
R : Type u_1
V : Type u_2
V' : Type ?u.236526
P : Type u_3
P' : Type ?u.236532
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'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : ¬x = y
⊢ Wbtw R x (↑(lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1
R : Type u_1
V : Type u_2
V' : Type ?u.236526
P : Type u_3
P' : Type ?u.236532
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'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ Wbtw R x (↑(lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1
by_cases hxy : x = y
no goals
case neg
R : Type u_1
V : Type u_2
V' : Type ?u.236526
P : Type u_3
P' : Type ?u.236532
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'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : ¬x = y
⊢ Wbtw R x (↑(lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1
rw [or_iff_right hxy, Wbtw, affineSegment, (lineMap_injective R hxy).mem_set_image]
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.236526
P : Type u_3
P' : Type ?u.236532
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'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ r ∈ Set.Icc 0 1
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.236526
P : Type u_3
P' : Type ?u.236532
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'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R x (↑(lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1
rw [hxy, lineMap_same_apply]
no goals
case pos
R : Type u_1
V : Type u_2
V' : Type ?u.236526
P : Type u_3
P' : Type ?u.236532
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'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ r ∈ Set.Icc 0 1
simp