case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c : 𝕜
⊢ openSegment 𝕜 x y ⊆
    insert (↑(lineMap x y) c) (openSegment 𝕜 x (↑(lineMap x y) c) ∪ openSegment 𝕜 (↑(lineMap x y) c) y)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z✝ x y z : E
hz : z ∈ range ↑(lineMap x y)
⊢ openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)
rcases hz with ⟨c, rfl⟩
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c : 𝕜
⊢ MapsTo (fun a => ↑(lineMap x y) a) (Ioo 0 1)
    (insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1))
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c : 𝕜
⊢ openSegment 𝕜 x y ⊆
    insert (↑(lineMap x y) c) (openSegment 𝕜 x (↑(lineMap x y) c) ∪ openSegment 𝕜 (↑(lineMap x y) c) y)
simp only [openSegment_eq_image_lineMap, ← mapsTo']
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1)
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c : 𝕜
⊢ MapsTo (fun a => ↑(lineMap x y) a) (Ioo 0 1)
    (insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1))
rintro a ⟨h₀, h₁⟩
case intro.intro.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1)

case intro.intro.inr.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) a)
      ((fun a_1 => ↑(lineMap x (↑(lineMap x y) a)) a_1) '' Ioo 0 1 ∪
        (fun a_1 => ↑(lineMap (↑(lineMap x y) a) y) a_1) '' Ioo 0 1)

case intro.intro.inr.inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1)
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1)
rcases lt_trichotomy a c with (hac | rfl | hca)
case intro.intro.inl.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (fun a => ↑(lineMap x y) a) a ∈
    (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
case intro.intro.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1)
right
case intro.intro.inl.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1
case intro.intro.inl.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (fun a => ↑(lineMap x y) a) a ∈
    (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
left
case intro.intro.inl.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1
case intro.intro.inl.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1
have hc : 0 < c := h₀.trans hac
case intro.intro.inl.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) (a / c) = (fun a => ↑(lineMap x y) a) a
case intro.intro.inl.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1
refine' ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, _⟩
no goals
case intro.intro.inl.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) (a / c) = (fun a => ↑(lineMap x y) a) a
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel _ hc.ne']
case intro.intro.inr.inl.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (fun a => ↑(lineMap x y) a) a = ↑(lineMap x y) a
case intro.intro.inr.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) a)
      ((fun a_1 => ↑(lineMap x (↑(lineMap x y) a)) a_1) '' Ioo 0 1 ∪
        (fun a_1 => ↑(lineMap (↑(lineMap x y) a) y) a_1) '' Ioo 0 1)
left
no goals
case intro.intro.inr.inl.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (fun a => ↑(lineMap x y) a) a = ↑(lineMap x y) a
rfl
case intro.intro.inr.inr.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (fun a => ↑(lineMap x y) a) a ∈
    (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
case intro.intro.inr.inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (fun a => ↑(lineMap x y) a) a ∈
    insert (↑(lineMap x y) c)
      ((fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪
        (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1)
right
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
case intro.intro.inr.inr.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (fun a => ↑(lineMap x y) a) a ∈
    (fun a => ↑(lineMap x (↑(lineMap x y) c)) a) '' Ioo 0 1 ∪ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
right
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z 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
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (fun a => ↑(lineMap x y) a) a ∈ (fun a => ↑(lineMap (↑(lineMap x y) c) y) a) '' Ioo 0 1
simp only [← lineMap_apply_one_sub y]
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (fun a => ↑(lineMap y (↑(lineMap y x) (1 - c))) (1 - a)) ((a - c) / (1 - c)) = ↑(lineMap y x) (1 - a)
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z 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
refine'
  ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
    _⟩
no goals
case intro.intro.inr.inr.h.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.220883
G : Type ?u.220886
ι : Type ?u.220889
π : ι → Type ?u.220894
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ y✝ z x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (fun a => ↑(lineMap y (↑(lineMap y x) (1 - c))) (1 - a)) ((a - c) / (1 - c)) = ↑(lineMap y x) (1 - a)
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul,
  div_mul_cancel _ hc.ne', sub_sub_sub_cancel_right]