case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
t : R
ht : t ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) t ≠ x
hyz : ↑(lineMap x z) t ≠ z
⊢ ↑(lineMap x z) t ∈ ↑(lineMap x z) '' Set.Ioo 0 1
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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 : Sbtw R x y z
⊢ y ∈ ↑(lineMap x z) '' Set.Ioo 0 1
rcases h with ⟨⟨t, ht, rfl⟩, hyx, hyz⟩
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 0 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 0 ≠ x
hyz : ↑(lineMap x z) 0 ≠ z
⊢ ↑(lineMap x z) 0 ∈ ↑(lineMap x z) '' Set.Ioo 0 1

case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 1 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 1 ≠ x
hyz : ↑(lineMap x z) 1 ≠ z
⊢ ↑(lineMap x z) 1 ∈ ↑(lineMap x z) '' Set.Ioo 0 1

case intro.intro.intro.intro.inr.inr
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
t : R
ht : t ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) t ≠ x
hyz : ↑(lineMap x z) t ≠ z
ho : t ∈ Set.Ioo 0 1
⊢ ↑(lineMap x z) t ∈ ↑(lineMap x z) '' Set.Ioo 0 1
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
t : R
ht : t ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) t ≠ x
hyz : ↑(lineMap x z) t ≠ z
⊢ ↑(lineMap x z) t ∈ ↑(lineMap x z) '' Set.Ioo 0 1
rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc ht with (rfl | rfl | ho)
case intro.intro.intro.intro.inl.h
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 0 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 0 ≠ x
hyz : ↑(lineMap x z) 0 ≠ z
⊢ False
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 0 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 0 ≠ x
hyz : ↑(lineMap x z) 0 ≠ z
⊢ ↑(lineMap x z) 0 ∈ ↑(lineMap x z) '' Set.Ioo 0 1
exfalso
no goals
case intro.intro.intro.intro.inl.h
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 0 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 0 ≠ x
hyz : ↑(lineMap x z) 0 ≠ z
⊢ False
exact hyx (lineMap_apply_zero _ _)
case intro.intro.intro.intro.inr.inl.h
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 1 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 1 ≠ x
hyz : ↑(lineMap x z) 1 ≠ z
⊢ False
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 1 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 1 ≠ x
hyz : ↑(lineMap x z) 1 ≠ z
⊢ ↑(lineMap x z) 1 ∈ ↑(lineMap x z) '' Set.Ioo 0 1
exfalso
no goals
case intro.intro.intro.intro.inr.inl.h
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
ht : 1 ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) 1 ≠ x
hyz : ↑(lineMap x z) 1 ≠ z
⊢ False
exact hyz (lineMap_apply_one _ _)
no goals
case intro.intro.intro.intro.inr.inr
R : Type u_1
V : Type u_2
V' : Type ?u.138137
P : Type u_3
P' : Type ?u.138143
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
t : R
ht : t ∈ Set.Icc 0 1
hyx : ↑(lineMap x z) t ≠ x
hyz : ↑(lineMap x z) t ≠ z
ho : t ∈ Set.Ioo 0 1
⊢ ↑(lineMap x z) t ∈ ↑(lineMap x z) '' Set.Ioo 0 1
exact ⟨t, ho, rfl⟩