-- Mathlib/Analysis/Convex/Between.lean
theorem Sbtw.mem_image_Ioo {x y z : P} (h : Sbtw R x y z) :
    y ∈ lineMap x z '' Set.Ioo (0 : R) 1

Proof state:
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Tactic:
exfalso

Result:
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Proof state:
case intro.intro.intro.intro.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Tactic:
exact ⟨t, ho, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Tactic:
exfalso

Result:
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Tactic:
rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc ht with (rfl | rfl | ho)

Result:
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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
P : Type u_4
inst✝³ : OrderedRing R
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
P : Type u_4
inst✝³ : OrderedRing R
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

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Tactic:
rcases h with ⟨⟨t, ht, rfl⟩, hyx, hyz⟩

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Proof state:
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Tactic:
exact hyz (lineMap_apply_one _ _)

Result:
no goals

Proof state:
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
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

Tactic:
exact hyx (lineMap_apply_zero _ _)

Result:
no goals