R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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 : P
⊢ affineSegment R x y = affineSegment R y x
refine' Set.ext fun z => _
case mpr.intro.intro
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
t : R
ht : t ∈ Set.Icc 0 1
hxy : ↑(lineMap y x) t = z
⊢ z ∈ affineSegment R x y
case mpr
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
⊢ z ∈ affineSegment R y x → z ∈ affineSegment R x y
rintro ⟨t, ht, hxy⟩
case mpr.intro.intro.refine'_1
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
t : R
ht : t ∈ Set.Icc 0 1
hxy : ↑(lineMap y x) t = z
⊢ 1 - t ∈ Set.Icc 0 1

case mpr.intro.intro.refine'_2
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
t : R
ht : t ∈ Set.Icc 0 1
hxy : ↑(lineMap y x) t = z
⊢ ↑(lineMap x y) (1 - t) = z
case mpr.intro.intro
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
t : R
ht : t ∈ Set.Icc 0 1
hxy : ↑(lineMap y x) t = z
⊢ z ∈ affineSegment R x y
refine' ⟨1 - t, _, _⟩
no goals
case mpr.intro.intro.refine'_1
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
t : R
ht : t ∈ Set.Icc 0 1
hxy : ↑(lineMap y x) t = z
⊢ 1 - t ∈ Set.Icc 0 1
rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
no goals
case mpr.intro.intro.refine'_2
R : Type u_2
V : Type u_3
V' : Type ?u.8362
P : Type u_1
P' : Type ?u.8368
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
t : R
ht : t ∈ Set.Icc 0 1
hxy : ↑(lineMap y x) t = z
⊢ ↑(lineMap x y) (1 - t) = z
rwa [lineMap_apply_one_sub]