[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
x✝ y✝ x y : E
⊢ [x-[𝕜]y] = (fun p => p.fst • x + p.snd • y) '' {p | 0 ≤ p.fst ∧ 0 ≤ p.snd ∧ p.fst + p.snd = 1}
[PROOFSTEP]
simp only [segment, image, Prod.exists, mem_setOf_eq, exists_prop, and_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
x✝ y✝ x y : E
⊢ openSegment 𝕜 x y = (fun p => p.fst • x + p.snd • y) '' {p | 0 < p.fst ∧ 0 < p.snd ∧ p.fst + p.snd = 1}
[PROOFSTEP]
simp only [openSegment, image, Prod.exists, mem_setOf_eq, exists_prop, and_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : MulActionWithZero 𝕜 E
x y : E
⊢ 1 • x + 0 • y = x
[PROOFSTEP]
rw [zero_smul, one_smul, add_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝¹ y z✝ x z : E
x✝ : z ∈ [x-[𝕜]x]
a b : 𝕜
w✝¹ : 0 ≤ a
w✝ : 0 ≤ b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}
[PROOFSTEP]
simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
⊢ insert x (insert y (openSegment 𝕜 x y)) = [x-[𝕜]y]
[PROOFSTEP]
simp only [subset_antisymm_iff, insert_subset_iff, left_mem_segment, right_mem_segment, openSegment_subset_segment,
  true_and_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
⊢ [x-[𝕜]y] ⊆ insert x (insert y (openSegment 𝕜 x y))
[PROOFSTEP]
rintro z ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
[PROOFSTEP]
refine' hb.eq_or_gt.imp _ fun hb' => ha.eq_or_gt.imp _ fun ha' => _
[GOAL]
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b = 0 → a • x + b • y = x
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ a • x + 0 • y = x
[PROOFSTEP]
rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
[GOAL]
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ a = 0 → a • x + b • y = y
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y = y
[PROOFSTEP]
rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
[GOAL]
case intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝ y✝ z x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y
[PROOFSTEP]
exact ⟨a, b, ha', hb', hab, rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ [x-[𝕜]y]
⊢ z ∈ openSegment 𝕜 x y
[PROOFSTEP]
rw [← insert_endpoints_openSegment] at hz
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ insert x (insert y (openSegment 𝕜 x y))
⊢ z ∈ openSegment 𝕜 x y
[PROOFSTEP]
exact (hz.resolve_left hx.symm).resolve_left hy.symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y z : E
hx : x ∈ s
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ s ↔ [x-[𝕜]y] ⊆ s
[PROOFSTEP]
simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
x✝ : z ∈ openSegment 𝕜 x x
a b : 𝕜
w✝¹ : 0 < a
w✝ : 0 < b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}
[PROOFSTEP]
simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
⊢ z ∈ openSegment 𝕜 x x
[PROOFSTEP]
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ z ∈ openSegment 𝕜 x x
[PROOFSTEP]
refine' ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, _⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ a • x + (1 - a) • x = z
[PROOFSTEP]
rw [← add_smul, add_sub_cancel'_right, one_smul, h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E
x✝ : z ∈ [x-[𝕜]y]
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
⊢ (fun θ => (a + b - θ) • x + θ • y) b = a • x + b • y
[PROOFSTEP]
simp only [add_sub_cancel]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E
x✝ : z ∈ openSegment 𝕜 x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ (fun θ => (a + b - θ) • x + θ • y) b = a • x + b • y
[PROOFSTEP]
simp only [add_sub_cancel]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
⊢ [x-[𝕜]y] = (fun θ => x + θ • (y - x)) '' Icc 0 1
[PROOFSTEP]
convert segment_eq_image 𝕜 x y using 2
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
[PROOFSTEP]
simp only [smul_sub, sub_smul, one_smul]
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
[PROOFSTEP]
abel
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
⊢ openSegment 𝕜 x y = (fun θ => x + θ • (y - x)) '' Ioo 0 1
[PROOFSTEP]
convert openSegment_eq_image 𝕜 x y using 2
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
[PROOFSTEP]
simp only [smul_sub, sub_smul, one_smul]
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
[PROOFSTEP]
abel
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
⊢ [x-[𝕜]y] = ↑(AffineMap.lineMap x y) '' Icc 0 1
[PROOFSTEP]
convert segment_eq_image 𝕜 x y using 2
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ ↑(AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y
[PROOFSTEP]
exact AffineMap.lineMap_apply_module _ _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
⊢ openSegment 𝕜 x y = ↑(AffineMap.lineMap x y) '' Ioo 0 1
[PROOFSTEP]
convert openSegment_eq_image 𝕜 x y using 2
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ ↑(AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y
[PROOFSTEP]
exact AffineMap.lineMap_apply_module _ _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ x ∈ ↑f '' [a-[𝕜]b] ↔ x ∈ [↑f a-[𝕜]↑f b]
[PROOFSTEP]
simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ x ∈ ↑f '' openSegment 𝕜 a b ↔ x ∈ openSegment 𝕜 (↑f a) (↑f b)
[PROOFSTEP]
simp_rw [openSegment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
a x b c : E
⊢ a + x ∈ [a + b-[𝕜]a + c] ↔ x ∈ [b-[𝕜]c]
[PROOFSTEP]
simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
a x b c : E
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c
[PROOFSTEP]
simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ [y-[𝕜]z]
⊢ SameRay 𝕜 (x - y) (z - x)
[PROOFSTEP]
rw [segment_eq_image'] at h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ (fun θ => y + θ • (z - y)) '' Icc 0 1
⊢ SameRay 𝕜 (x - y) (z - x)
[PROOFSTEP]
rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
θ : 𝕜
hθ₀ : 0 ≤ θ
hθ₁ : θ ≤ 1
⊢ SameRay 𝕜 ((fun θ => y + θ • (z - y)) θ - y) (z - (fun θ => y + θ • (z - y)) θ)
[PROOFSTEP]
simpa only [add_sub_cancel', ← sub_sub, sub_smul, one_smul] using
  (SameRay.sameRay_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ [x-[𝕜]y]
[PROOFSTEP]
rw [segment_eq_image_lineMap]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ ↑(AffineMap.lineMap x y) '' Icc 0 1
[PROOFSTEP]
exact ⟨⅟2, ⟨invOf_nonneg.mpr zero_le_two, invOf_le_one one_le_two⟩, rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ x ∈ [x - y-[𝕜]x + y]
[PROOFSTEP]
convert @midpoint_mem_segment 𝕜 _ _ _ _ _ _ _
[GOAL]
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)
[PROOFSTEP]
rw [midpoint_sub_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ x ∈ [x + y-[𝕜]x - y]
[PROOFSTEP]
convert @midpoint_mem_segment 𝕜 _ _ _ _ _ _ _
[GOAL]
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x + y) (x - y)
[PROOFSTEP]
rw [midpoint_add_sub]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x y → x = y
[PROOFSTEP]
rintro ⟨a, b, _, hb, hab, hx⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
a b : 𝕜
w✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ x = y
[PROOFSTEP]
refine' smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 _)
[GOAL]
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
a b : 𝕜
w✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ a • x + (fun x x_1 => x • x_1) b x = a • x + (fun x x_1 => x • x_1) b y
[PROOFSTEP]
rw [hx, ← add_smul, hab, one_smul]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x = y → x ∈ openSegment 𝕜 x y
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x x
[PROOFSTEP]
rw [openSegment_same]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ {x}
[PROOFSTEP]
exact mem_singleton _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ y ∈ openSegment 𝕜 x y ↔ x = y
[PROOFSTEP]
rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y-[𝕜]z] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y-[𝕜]z] → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
[PROOFSTEP]
rintro ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 ≤ b_1 ∧ 0 < a_1 + b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
[PROOFSTEP]
use a, b, ha, hb
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
[PROOFSTEP]
simp [*]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y-[𝕜]z]
[PROOFSTEP]
rintro ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ [y-[𝕜]z]
[PROOFSTEP]
refine' ⟨a / (a + b), b / (a + b), by positivity, by positivity, _, rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ a / (a + b)
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ b / (a + b)
[PROOFSTEP]
positivity
[GOAL]
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1
[PROOFSTEP]
rw [← add_div, div_self hab.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z ↔ ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z → ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
[PROOFSTEP]
rintro ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 < a_1 ∧ 0 < b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
[PROOFSTEP]
use a, b, ha, hb
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
[PROOFSTEP]
rw [hab, div_one, div_one]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z
[PROOFSTEP]
rintro ⟨a, b, ha, hb, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
[PROOFSTEP]
have hab : 0 < a + b := by positivity
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < a + b
[PROOFSTEP]
positivity
[GOAL]
case mpr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
[PROOFSTEP]
refine' ⟨a / (a + b), b / (a + b), by positivity, by positivity, _, rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < a / (a + b)
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < b / (a + b)
[PROOFSTEP]
positivity
[GOAL]
case mpr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1
[PROOFSTEP]
rw [← add_div, div_self hab.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y-[𝕜]z] ↔ SameRay 𝕜 (x - y) (z - x)
[PROOFSTEP]
refine' ⟨sameRay_of_mem_segment, fun h => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
⊢ x ∈ [y-[𝕜]z]
[PROOFSTEP]
rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (x - y + (z - x))
hzx : z - x = b • (x - y + (z - x))
⊢ x ∈ [y-[𝕜]z]
[PROOFSTEP]
rw [add_comm, sub_add_sub_cancel] at hxy hzx
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ x ∈ [y-[𝕜]z]
[PROOFSTEP]
rw [← mem_segment_translate _ (-x), neg_add_self]
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ 0 ∈ [-x + y-[𝕜]-x + z]
[PROOFSTEP]
refine' ⟨b, a, hb, ha, add_comm a b ▸ hab, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ b • (-x + y) + a • (-x + z) = 0
[PROOFSTEP]
rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_self]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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)
[PROOFSTEP]
rcases hz with ⟨c, rfl⟩
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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)
[PROOFSTEP]
simp only [openSegment_eq_image_lineMap, ← mapsTo']
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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))
[PROOFSTEP]
rintro a ⟨h₀, h₁⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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)
[PROOFSTEP]
rcases lt_trichotomy a c with (hac | rfl | hca)
[GOAL]
case intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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)
[PROOFSTEP]
right
[GOAL]
case intro.intro.inl.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
left
[GOAL]
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
have hc : 0 < c := h₀.trans hac
[GOAL]
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
refine' ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, _⟩
[GOAL]
case intro.intro.inl.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel _ hc.ne']
[GOAL]
case intro.intro.inr.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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)
[PROOFSTEP]
left
[GOAL]
case intro.intro.inr.inl.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.inr.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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)
[PROOFSTEP]
right
[GOAL]
case intro.intro.inr.inr.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
right
[GOAL]
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
[GOAL]
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
simp only [← lineMap_apply_one_sub y]
[GOAL]
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
refine' ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩, _⟩
[GOAL]
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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)
[PROOFSTEP]
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul, div_mul_cancel _ hc.ne',
  sub_sub_sub_cancel_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ Icc x y
[PROOFSTEP]
rintro z ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Icc x y
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.intro.intro.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ x ≤ a • x + b • y
case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ y
[PROOFSTEP]
calc
  x = a • x + b • x := (Convex.combo_self hab _).symm
  _ ≤ a • x + b • y := by gcongr
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • x ≤ a • x + b • y
[PROOFSTEP]
gcongr
[GOAL]
case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ y
[PROOFSTEP]
calc
  a • x + b • y ≤ a • y + b • y := by gcongr
  _ = y := Convex.combo_self hab _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ a • y + b • y
[PROOFSTEP]
gcongr
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
⊢ openSegment 𝕜 x y ⊆ Ioo x y
[PROOFSTEP]
rintro z ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ Ioo x y
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.intro.intro.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a • x + b • y
case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y
[PROOFSTEP]
calc
  x = a • x + b • x := (Convex.combo_self hab _).symm
  _ < a • x + b • y := by gcongr
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • x < a • x + b • y
[PROOFSTEP]
gcongr
[GOAL]
case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y
[PROOFSTEP]
calc
  a • x + b • y < a • y + b • y := by gcongr
  _ = y := Convex.combo_self hab _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < a • y + b • y
[PROOFSTEP]
gcongr
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
⊢ [x-[𝕜]y] ⊆ uIcc x y
[PROOFSTEP]
cases' le_total x y with h h
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ uIcc x y
[PROOFSTEP]
rw [uIcc_of_le h]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ Icc x y
[PROOFSTEP]
exact segment_subset_Icc h
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : y ≤ x
⊢ [x-[𝕜]y] ⊆ uIcc x y
[PROOFSTEP]
rw [uIcc_of_ge h, segment_symm]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
a b : 𝕜
x y : E
h : y ≤ x
⊢ [y-[𝕜]x] ⊆ Icc y x
[PROOFSTEP]
exact segment_subset_Icc h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
⊢ Icc x y ⊆ [x-[𝕜]y]
[PROOFSTEP]
rintro z ⟨hxz, hyz⟩
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
⊢ z ∈ [x-[𝕜]y]
[PROOFSTEP]
obtain rfl | h := (hxz.trans hyz).eq_or_lt
[GOAL]
case intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x-[𝕜]x]
[PROOFSTEP]
rw [segment_same]
[GOAL]
case intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ {x}
[PROOFSTEP]
exact hyz.antisymm hxz
[GOAL]
case intro.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z✝ z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x-[𝕜]y]
[PROOFSTEP]
rw [← sub_nonneg] at hxz hyz
[GOAL]
case intro.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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]
[PROOFSTEP]
rw [← sub_pos] at h
[GOAL]
case intro.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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]
[PROOFSTEP]
refine' ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, _, _⟩
[GOAL]
case intro.inr.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
rw [← add_div, sub_add_sub_cancel, div_self h.ne']
[GOAL]
case intro.inr.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
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
[PROOFSTEP]
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]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x✝ y✝ z x y : 𝕜
⊢ [x-[𝕜]y] = Icc (min x y) (max x y)
[PROOFSTEP]
cases' le_total x y with h h
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x✝ y✝ z x y : 𝕜
h : x ≤ y
⊢ [x-[𝕜]y] = Icc (min x y) (max x y)
[PROOFSTEP]
rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x✝ y✝ z x y : 𝕜
h : y ≤ x
⊢ [x-[𝕜]y] = Icc (min x y) (max x y)
[PROOFSTEP]
rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
[PROOFSTEP]
cases' hxy.lt_or_lt with h h
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
h : x < y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
[PROOFSTEP]
rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
[PROOFSTEP]
rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
rw [← segment_eq_Icc h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ [x-[𝕜]y] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
simp_rw [← exists_prop]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ [x-[𝕜]y] ↔ ∃ a b _h _h _h, a * x + b * y = z
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
rw [← openSegment_eq_Ioo h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ openSegment 𝕜 x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
simp_rw [← exists_prop]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ openSegment 𝕜 x y ↔ ∃ a b _h _h _h, a * x + b * y = z
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
refine' ⟨fun hz => _, _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
hz : z ∈ Ioc x y
⊢ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
[PROOFSTEP]
obtain rfl | hb' := hb.eq_or_lt
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a + 0 = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
[PROOFSTEP]
rw [add_zero] at hab
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
[PROOFSTEP]
rw [hab, one_mul, zero_mul, add_zero] at hz
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : x ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
[PROOFSTEP]
exact (hz.1.ne rfl).elim
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
hb' : 0 < b
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
[PROOFSTEP]
exact ⟨a, b, ha, hb', hab, rfl⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ioc x y
[PROOFSTEP]
rintro ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a * x + b * y ∈ Ioc x y
[PROOFSTEP]
obtain rfl | ha' := ha.eq_or_lt
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 * x + b * y ∈ Ioc x y
[PROOFSTEP]
rw [zero_add] at hab
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 * x + b * y ∈ Ioc x y
[PROOFSTEP]
rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
ha' : 0 < a
⊢ a * x + b * y ∈ Ioc x y
[PROOFSTEP]
exact Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ico x y ↔ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
refine' ⟨fun hz => _, _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
hz : z ∈ Ico x y
⊢ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
[PROOFSTEP]
obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ico_subset_Icc_self hz)
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ico x y
⊢ ∃ a_1 b_1, 0 < a_1 ∧ 0 ≤ b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
[PROOFSTEP]
obtain rfl | ha' := ha.eq_or_lt
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
hz : 0 * x + b * y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y
[PROOFSTEP]
rw [zero_add] at hab
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
hz : 0 * x + b * y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y
[PROOFSTEP]
rw [hab, one_mul, zero_mul, zero_add] at hz
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
hz : y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y
[PROOFSTEP]
exact (hz.2.ne rfl).elim
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ico x y
ha' : 0 < a
⊢ ∃ a_1 b_1, 0 < a_1 ∧ 0 ≤ b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
[PROOFSTEP]
exact ⟨a, b, ha', hb, hab, rfl⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ico x y
[PROOFSTEP]
rintro ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * x + b * y ∈ Ico x y
[PROOFSTEP]
obtain rfl | hb' := hb.eq_or_lt
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 < a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ a * x + 0 * y ∈ Ico x y
[PROOFSTEP]
rw [add_zero] at hab
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 < a
hb : 0 ≤ 0
hab : a = 1
⊢ a * x + 0 * y ∈ Ico x y
[PROOFSTEP]
rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ a * x + b * y ∈ Ico x y
[PROOFSTEP]
exact Ioo_subset_Ico_self ((Convex.mem_Ioo h).2 ⟨a, b, ha, hb', hab, rfl⟩)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ [x-[𝕜]y] ⊆ [x.fst-[𝕜]y.fst] ×ˢ [x.snd-[𝕜]y.snd]
[PROOFSTEP]
rintro z ⟨a, b, ha, hb, hab, hz⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ [x.fst-[𝕜]y.fst] ×ˢ [x.snd-[𝕜]y.snd]
[PROOFSTEP]
exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ openSegment 𝕜 x y ⊆ openSegment 𝕜 x.fst y.fst ×ˢ openSegment 𝕜 x.snd y.snd
[PROOFSTEP]
rintro z ⟨a, b, ha, hb, hab, hz⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x.fst y.fst ×ˢ openSegment 𝕜 x.snd y.snd
[PROOFSTEP]
exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x, y)) '' [x₁-[𝕜]x₂] = [(x₁, y)-[𝕜](x₂, y)]
[PROOFSTEP]
ext ⟨x', y'⟩
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
x' : E
y' : F
⊢ (x', y') ∈ (fun x => (x, y)) '' [x₁-[𝕜]x₂] ↔ (x', y') ∈ [(x₁, y)-[𝕜](x₂, y)]
[PROOFSTEP]
simp_rw [Set.mem_image, segment, Set.mem_setOf, Prod.smul_mk, Prod.mk_add_mk, Prod.mk.inj_iff, ← exists_and_right,
  @exists_comm E, exists_eq_left']
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
x' : E
y' : F
⊢ (∃ b b_1 h h h, b • x₁ + b_1 • x₂ = x' ∧ y = y') ↔ ∃ a b h h h, a • x₁ + b • x₂ = x' ∧ a • y + b • y = y'
[PROOFSTEP]
refine' exists₅_congr fun a b ha hb hab => _
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
x' : E
y' : F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x₁ + b • x₂ = x' ∧ y = y' ↔ a • x₁ + b • x₂ = x' ∧ a • y + b • y = y'
[PROOFSTEP]
rw [Convex.combo_self hab]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun y => (x, y)) '' [y₁-[𝕜]y₂] = [(x, y₁)-[𝕜](x, y₂)]
[PROOFSTEP]
ext ⟨x', y'⟩
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (x', y') ∈ (fun y => (x, y)) '' [y₁-[𝕜]y₂] ↔ (x', y') ∈ [(x, y₁)-[𝕜](x, y₂)]
[PROOFSTEP]
simp_rw [Set.mem_image, segment, Set.mem_setOf, Prod.smul_mk, Prod.mk_add_mk, Prod.mk.inj_iff, ← exists_and_right,
  @exists_comm F, exists_eq_left']
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (∃ b b_1 h h h, x = x' ∧ b • y₁ + b_1 • y₂ = y') ↔ ∃ a b h h h, a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
[PROOFSTEP]
refine' exists₅_congr fun a b ha hb hab => _
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ x = x' ∧ a • y₁ + b • y₂ = y' ↔ a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
[PROOFSTEP]
rw [Convex.combo_self hab]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)
[PROOFSTEP]
ext ⟨x', y'⟩
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
x' : E
y' : F
⊢ (x', y') ∈ (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ ↔ (x', y') ∈ openSegment 𝕜 (x₁, y) (x₂, y)
[PROOFSTEP]
simp_rw [Set.mem_image, openSegment, Set.mem_setOf, Prod.smul_mk, Prod.mk_add_mk, Prod.mk.inj_iff, ← exists_and_right,
  @exists_comm E, exists_eq_left']
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
x' : E
y' : F
⊢ (∃ b b_1 h h h, b • x₁ + b_1 • x₂ = x' ∧ y = y') ↔ ∃ a b h h h, a • x₁ + b • x₂ = x' ∧ a • y + b • y = y'
[PROOFSTEP]
refine' exists₅_congr fun a b ha hb hab => _
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
x' : E
y' : F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x₁ + b • x₂ = x' ∧ y = y' ↔ a • x₁ + b • x₂ = x' ∧ a • y + b • y = y'
[PROOFSTEP]
rw [Convex.combo_self hab]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)
[PROOFSTEP]
ext ⟨x', y'⟩
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (x', y') ∈ (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ ↔ (x', y') ∈ openSegment 𝕜 (x, y₁) (x, y₂)
[PROOFSTEP]
simp_rw [Set.mem_image, openSegment, Set.mem_setOf, Prod.smul_mk, Prod.mk_add_mk, Prod.mk.inj_iff, ← exists_and_right,
  @exists_comm F, exists_eq_left']
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (∃ b b_1 h h h, x = x' ∧ b • y₁ + b_1 • y₂ = y') ↔ ∃ a b h h h, a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
[PROOFSTEP]
refine' exists₅_congr fun a b ha hb hab => _
[GOAL]
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x = x' ∧ a • y₁ + b • y₂ = y' ↔ a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
[PROOFSTEP]
rw [Convex.combo_self hab]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y : (i : ι) → π i
⊢ [x-[𝕜]y] ⊆ pi s fun i => [x i-[𝕜]y i]
[PROOFSTEP]
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => [x i-[𝕜]y i]) i
[PROOFSTEP]
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y : (i : ι) → π i
⊢ openSegment 𝕜 x y ⊆ pi s fun i => openSegment 𝕜 (x i) (y i)
[PROOFSTEP]
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => openSegment 𝕜 (x i) (y i)) i
[PROOFSTEP]
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ update y i '' [x₁-[𝕜]x₂] = [update y i x₁-[𝕜]update y i x₂]
[PROOFSTEP]
ext z
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ z ∈ update y i '' [x₁-[𝕜]x₂] ↔ z ∈ [update y i x₁-[𝕜]update y i x₂]
[PROOFSTEP]
simp_rw [Set.mem_image, segment, Set.mem_setOf, ← update_smul, ← update_add, update_eq_iff, ← exists_and_right,
  @exists_comm (π i), exists_eq_left']
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ (∃ b b_1 h h h, b • x₁ + b_1 • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    ∃ a b h h h, a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
[PROOFSTEP]
refine' exists₅_congr fun a b ha hb hab => _
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
[PROOFSTEP]
rw [Convex.combo_self hab]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂)
[PROOFSTEP]
ext z
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ z ∈ update y i '' openSegment 𝕜 x₁ x₂ ↔ z ∈ openSegment 𝕜 (update y i x₁) (update y i x₂)
[PROOFSTEP]
simp_rw [Set.mem_image, openSegment, Set.mem_setOf, ← update_smul, ← update_add, update_eq_iff, ← exists_and_right,
  @exists_comm (π i), exists_eq_left']
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ (∃ b b_1 h h h, b • x₁ + b_1 • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    ∃ a b h h h, a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
[PROOFSTEP]
refine' exists₅_congr fun a b ha hb hab => _
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
[PROOFSTEP]
rw [Convex.combo_self hab]


[GOAL]
x : ℝ
hx : x ≤ 0
⊢ expNegInvGlue x = 0
[PROOFSTEP]
simp [expNegInvGlue, hx]
[GOAL]
x : ℝ
hx : 0 < x
⊢ 0 < expNegInvGlue x
[PROOFSTEP]
simp [expNegInvGlue, not_le.2 hx, exp_pos]
[GOAL]
x : ℝ
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
cases le_or_gt x 0 with
| inl h => exact ge_of_eq (zero_of_nonpos h)
| inr h => exact le_of_lt (pos_of_pos h)
[GOAL]
x : ℝ
x✝ : x ≤ 0 ∨ x > 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
cases le_or_gt x 0 with
| inl h => exact ge_of_eq (zero_of_nonpos h)
| inr h => exact le_of_lt (pos_of_pos h)
[GOAL]
case inl
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]

| inl h => exact ge_of_eq (zero_of_nonpos h)
[GOAL]
case inl
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
exact ge_of_eq (zero_of_nonpos h)
[GOAL]
case inr
x : ℝ
h : x > 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]

| inr h => exact le_of_lt (pos_of_pos h)
[GOAL]
case inr
x : ℝ
h : x > 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
exact le_of_lt (pos_of_pos h)
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
simp only [expNegInvGlue, mul_ite, mul_zero]
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0) (𝓝 0)
[PROOFSTEP]
refine tendsto_const_nhds.if ?_
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | ¬x ≤ 0}) (𝓝 0)
[PROOFSTEP]
simp only [not_le]
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun x ↦ p.eval x⁻¹ / exp x⁻¹) (𝓝[>] 0) (𝓝 0) := p.tendsto_div_exp_atTop.comp tendsto_inv_zero_atTop
[GOAL]
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
[PROOFSTEP]
refine this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_
[GOAL]
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹) (𝓝[Ioi 0] 0) (𝓝 0)
x : ℝ
hx : x ∈ {x | 0 < x}
⊢ x ∈ {x | (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹ = (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) x) x}
[PROOFSTEP]
simp [expNegInvGlue, hx.out.not_le, exp_neg, div_eq_mul_inv]
[GOAL]
p : ℝ[X]
x : ℝ
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
[PROOFSTEP]
rcases lt_trichotomy x 0 with hx | rfl | hx
[GOAL]
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
[PROOFSTEP]
rw [zero_of_nonpos hx.le, mul_zero]
[GOAL]
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
[PROOFSTEP]
refine (hasDerivAt_const _ 0).congr_of_eventuallyEq ?_
[GOAL]
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] fun x => 0
[PROOFSTEP]
filter_upwards [gt_mem_nhds hx] with y hy
[GOAL]
case h
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
[PROOFSTEP]
rw [zero_of_nonpos hy.le, mul_zero]
[GOAL]
case inr.inl
p : ℝ[X]
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval 0⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue 0) 0
[PROOFSTEP]
rw [expNegInvGlue.zero, mul_zero, hasDerivAt_iff_tendsto_slope]
[GOAL]
case inr.inl
p : ℝ[X]
⊢ Tendsto (slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[{0}ᶜ] 0) (𝓝 0)
[PROOFSTEP]
refine ((tendsto_polynomial_inv_mul_zero (p * X)).mono_left inf_le_left).congr fun x ↦ ?_
[GOAL]
case inr.inl
p : ℝ[X]
x : ℝ
⊢ Polynomial.eval x⁻¹ (p * X) * expNegInvGlue x = slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
[PROOFSTEP]
simp [slope_def_field, div_eq_mul_inv, mul_right_comm]
[GOAL]
case inr.inr
p : ℝ[X]
x : ℝ
hx : 0 < x
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
[PROOFSTEP]
have := ((p.hasDerivAt x⁻¹).mul (hasDerivAt_neg _).exp).comp x (hasDerivAt_inv hx.ne')
[GOAL]
case inr.inr
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
[PROOFSTEP]
convert this.congr_of_eventuallyEq _ using 1
[GOAL]
case h.e'_7
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x =
    (Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹
[PROOFSTEP]
simp [expNegInvGlue, hx.not_le]
[GOAL]
case h.e'_7
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ (x ^ 2)⁻¹ * (Polynomial.eval x⁻¹ p - Polynomial.eval x⁻¹ (↑derivative p)) * exp (-x⁻¹) =
    -((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + -(Polynomial.eval x⁻¹ p * exp (-x⁻¹))) * (x ^ 2)⁻¹)
[PROOFSTEP]
ring
[GOAL]
case inr.inr.convert_2
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] (fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv
[PROOFSTEP]
filter_upwards [lt_mem_nhds hx] with y hy
[GOAL]
case h
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
y : ℝ
hy : 0 < y
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv) y
[PROOFSTEP]
simp [expNegInvGlue, hy.not_le]
[GOAL]
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ n fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
apply contDiff_all_iff_nat.2 (fun m => ?_) n
[GOAL]
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
induction m generalizing p with
| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
| succ m ihm =>
  refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
  convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
  exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
induction m generalizing p with
| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
| succ m ihm =>
  refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
  convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
  exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
case zero
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑Nat.zero fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]

| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
[GOAL]
case zero
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑Nat.zero fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
[GOAL]
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ ↑(Nat.succ m) fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]

| succ m ihm =>
  refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
  convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
  exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ ↑(Nat.succ m) fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
[GOAL]
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (↑m) (deriv fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
[PROOFSTEP]
convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
[GOAL]
case h.e'_10.h
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
x✝ : ℝ
⊢ deriv (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) x✝ =
    Polynomial.eval x✝⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x✝
[PROOFSTEP]
exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
n : ℕ∞
⊢ ContDiff ℝ n expNegInvGlue
[PROOFSTEP]
simpa using contDiff_polynomial_eval_inv_mul 1
[GOAL]
x : ℝ
h : 1 ≤ x
⊢ expNegInvGlue x = expNegInvGlue x + expNegInvGlue (1 - x)
[PROOFSTEP]
rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]
[GOAL]
x : ℝ
⊢ smoothTransition x = 0 ↔ x ≤ 0
[PROOFSTEP]
simp only [smoothTransition, _root_.div_eq_zero_iff, (pos_denom x).ne', zero_iff_nonpos, or_false]
[GOAL]
x : ℝ
⊢ smoothTransition ↑(projIcc 0 1 (_ : 0 ≤ 1) x) = smoothTransition x
[PROOFSTEP]
refine' congr_fun (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => _) fun x hx => _) x
[GOAL]
case refine'_1
x✝ x : ℝ
hx : x < 0
⊢ smoothTransition x = smoothTransition 0
[PROOFSTEP]
rw [smoothTransition.zero, zero_of_nonpos hx.le]
[GOAL]
case refine'_2
x✝ x : ℝ
hx : 1 < x
⊢ smoothTransition x = smoothTransition 1
[PROOFSTEP]
rw [smoothTransition.one, one_of_one_le hx.le]


[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ HasDerivAt exp (exp x) x
[PROOFSTEP]
rw [hasDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
[PROOFSTEP]
have : (1 : ℕ) < 2 := by norm_num
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
[PROOFSTEP]
refine' (IsBigO.of_bound ‖exp x‖ _).trans_isLittleO (isLittleO_pow_id this)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖exp (x + x_1) - exp x - x_1 • exp x‖ ≤ ‖exp x‖ * ‖x_1 ^ 2‖
[PROOFSTEP]
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]
[GOAL]
case h
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), a ∈ Metric.ball 0 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a ^ 2‖
[PROOFSTEP]
simp only [Metric.mem_ball, dist_zero_right, norm_pow]
[GOAL]
case h
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a‖ ^ 2
[PROOFSTEP]
exact fun z hz => exp_bound_sq x z hz.le
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ deriv^[n + 1] exp = exp
[PROOFSTEP]
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
⊢ ∀ {n : ℕ∞}, ContDiff 𝕜 n exp
[PROOFSTEP]
refine' @(contDiff_all_iff_nat.2 fun n => ?_)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ ContDiff 𝕜 (↑n) exp
[PROOFSTEP]
have : ContDiff ℂ (↑n) exp := by
  induction' n with n ihn
  · exact contDiff_zero.2 continuous_exp
  · rw [contDiff_succ_iff_deriv]
    use differentiable_exp
    rwa [deriv_exp]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ ContDiff ℂ (↑n) exp
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
⊢ ContDiff ℂ (↑Nat.zero) exp
[PROOFSTEP]
exact contDiff_zero.2 continuous_exp
[GOAL]
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑(Nat.succ n)) exp
[PROOFSTEP]
rw [contDiff_succ_iff_deriv]
[GOAL]
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ Differentiable ℂ exp ∧ ContDiff ℂ (↑n) (deriv exp)
[PROOFSTEP]
use differentiable_exp
[GOAL]
case right
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑n) (deriv exp)
[PROOFSTEP]
rwa [deriv_exp]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
this : ContDiff ℂ (↑n) exp
⊢ ContDiff 𝕜 (↑n) exp
[PROOFSTEP]
exact this.restrict_scalars 𝕜
[GOAL]
x y z : ℝ
n : ℕ
⊢ deriv^[n + 1] exp = exp
[PROOFSTEP]
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]