case intro
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
⊢ z ∈ [x-[𝕜]y]
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
⊢ Icc x y ⊆ [x-[𝕜]y]
rintro z ⟨hxz, hyz⟩
case intro.inl
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x-[𝕜]x]

case intro.inr
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x-[𝕜]y]
case intro
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
⊢ z ∈ [x-[𝕜]y]
obtain rfl | h := (hxz.trans hyz).eq_or_lt
case intro.inr
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h : x < y
⊢ z ∈ [x-[𝕜]y]
case intro.inr
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x-[𝕜]y]
rw [← sub_nonneg] at hxz hyz
case intro.inr
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h✝ : x < y
h : 0 < y - x
⊢ z ∈ [x-[𝕜]y]
case intro.inr
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h : x < y
⊢ z ∈ [x-[𝕜]y]
rw [← sub_pos] at h
case intro.inr.refine'_1
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h✝ : x < y
h : 0 < y - x
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1

case intro.inr.refine'_2
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h✝ : x < y
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
case intro.inr
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h✝ : x < y
h : 0 < y - x
⊢ z ∈ [x-[𝕜]y]
refine' ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, _, _⟩
case intro.inl
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ {x}
case intro.inl
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x-[𝕜]x]
rw [segment_same]
no goals
case intro.inl
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ {x}
exact hyz.antisymm hxz
no goals
case intro.inr.refine'_1
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h✝ : x < y
h : 0 < y - x
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1
rw [← add_div, sub_add_sub_cancel, div_self h.ne']
no goals
case intro.inr.refine'_2
𝕜 : Type u_1
E : Type ?u.284099
F : Type ?u.284102
G : Type ?u.284105
ι : Type ?u.284108
π : ι → Type ?u.284113
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz✝ : x ≤ z
hxz : 0 ≤ z - x
hyz✝ : z ≤ y
hyz : 0 ≤ y - z
h✝ : x < y
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
rw [smul_eq_mul, smul_eq_mul, ← mul_div_right_comm, ← mul_div_right_comm, ← add_div,
  div_eq_iff h.ne', add_comm, sub_mul, sub_mul, mul_comm x, sub_add_sub_cancel, mul_sub]