𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
⊢ x ∈ [y-[𝕜]z]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y-[𝕜]z] ↔ SameRay 𝕜 (x - y) (z - x)
refine' ⟨sameRay_of_mem_segment, fun h => _⟩
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
⊢ x ∈ [y-[𝕜]z]
rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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]
rw [add_comm, sub_add_sub_cancel] at hxy hzx
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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]
rw [← mem_segment_translate _ (-x), neg_add_self]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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]
refine' ⟨b, a, hb, ha, add_comm a b ▸ hab, _⟩
no goals
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.214396
G : Type ?u.214399
ι : Type ?u.214402
π : ι → Type ?u.214407
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
rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_self]