-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_subset_union (x y : E) {z : E} (hz : z ∈ range (lineMap x y : 𝕜 → E)) :
    openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c : 𝕜
⊢ openSegment 𝕜 x y ⊆ insert ((lineMap x y) c) (openSegment 𝕜 x ((lineMap x y) c) ∪ openSegment 𝕜 ((lineMap x y) c) y)

Tactic:
simp only [openSegment_eq_image_lineMap, ← mapsTo']

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c : 𝕜
⊢ MapsTo (⇑(lineMap x y)) (Ioo 0 1)
    (insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1))

Proof state:
case intro.intro.inr.inr.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Tactic:
right

Result:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
hz : z ∈ range ⇑(lineMap x y)
⊢ openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

Tactic:
rcases hz with ⟨c, rfl⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c : 𝕜
⊢ openSegment 𝕜 x y ⊆ insert ((lineMap x y) c) (openSegment 𝕜 x ((lineMap x y) c) ∪ openSegment 𝕜 ((lineMap x y) c) y)

Proof state:
case intro.intro.inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

Tactic:
right

Result:
case intro.intro.inr.inr.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Proof state:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (lineMap x y) a ∈ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Tactic:
simp only [← lineMap_apply_one_sub y]

Result:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (lineMap y x) (1 - a) ∈ (fun a => (lineMap y ((lineMap y x) (1 - c))) (1 - a)) '' Ioo 0 1

Proof state:
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1

Tactic:
refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩

Result:
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (lineMap x ((lineMap x y) c)) (a / c) = (lineMap x y) a

Proof state:
case intro.intro.inr.inl.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a = (lineMap x y) a

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (lineMap x ((lineMap x y) c)) (a / c) = (lineMap x y) a

Tactic:
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']

Result:
no goals

Proof state:
case intro.intro.inl.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Tactic:
left

Result:
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1

Proof state:
case intro.intro.inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) a) (⇑(lineMap x ((lineMap x y) a)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) a) y) '' Ioo 0 1)

Tactic:
left

Result:
case intro.intro.inr.inl.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a = (lineMap x y) a

Proof state:
case intro.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

Tactic:
right

Result:
case intro.intro.inl.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Proof state:
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1

Tactic:
have hc : 0 < c := h₀.trans hac

Result:
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

Tactic:
rcases lt_trichotomy a c with (hac | rfl | hca)

Result:
case intro.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

case intro.intro.inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) a) (⇑(lineMap x ((lineMap x y) a)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) a) y) '' Ioo 0 1)

case intro.intro.inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)